Cooperation in Theorem Proving by Loosely Coupled Heuristics

  • We present a cooperation concept for automated theorem provers that isbased on a periodical interchange of selected results between several incarnationsof a prover. These incarnations differ from each other in the search heuristic theyemploy for guiding the search of the prover. Depending on the strengths' andweaknesses of these heuristics different knowledge and different communicationstructures are used for selecting the results to interchange.Our concept is easy to implement and can easily be integrated into alreadyexisting theorem provers. Moreover, the resulting cooperation allows the dis-tributed system to find proofs much faster than single heuristics working alone.We substantiate these claims by two case studies: experiments with the DiCoDesystem that is based on the condensed detachment rule and experiments with theSPASS system, a prover for first order logic with equality based on the super-position calculus. Both case studies show the improvements by our cooperationconcept.

Volltext Dateien herunterladen

Metadaten exportieren

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:Dirk Fuchs, Jörg Denzinger
URN (Permalink):urn:nbn:de:hbz:386-kluedo-3740
Schriftenreihe (Bandnummer):SEKI Report (97,3)
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:1999
Jahr der Veröffentlichung:1999
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.04.2000
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011