Inference Rights for Controlling Search in Generating Theorem Provers

  • We investigate the usage of so-called inference rights. We point out the prob-lems arising from the inflexibility of existing approaches to heuristically controlthe search of automated deduction systems, and we propose the application ofinference rights that are well-suited for controlling the search more flexibly. More-over, inference rights allow for a mechanism of "partial forgetting" of facts thatis not realizable in the most controlling aproaches. We study theoretical founda-tions of inference rights as well as the integration of inference rights into alreadyexisting inference systems. Furthermore, we present possibilities to control suchmodified inference systems in order to gain efficiency. Finally, we report onexperimental results obtained in the area of condensed detachment.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Dirk Fuchs
URN (Permalink):urn:nbn:de:hbz:386-kluedo-3691
Schriftenreihe (Bandnummer):SEKI Report (96,12)
Dokumentart:Preprint
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:1996
Jahr der Veröffentlichung:1996
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.04.2000
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $