Knowledge-based Cooperation between Theorem Provers by Techs

  • We present a methodology for coupling several saturation-based theoremprovers (running on different computers). The methodology is well-suited for re-alizing cooperation between different incarnations of one basic prover. Moreover,also different heterogeneous provers - that differ from each other in the calculusand in the heuristic they employ - can be coupled. Cooperation between the dif-ferent provers is achieved by periodically interchanging clauses which are selectedby so-called referees. We present theoretic results regarding the completeness ofthe system of cooperating provers as well as describe concrete heuristics for de-signing referees. Furthermore, we report on two experimental studies performedwith homogeneous and heterogeneous provers in the areas superposition and un-failing completion. The results reveal that the occurring synergetic effects leadto a significant improvement of performance.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Dirk Fuchs, Jörg Denzinger
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3829
Serie (Series number):SEKI Report (97,11)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $