Goal oriented equational theorem proving using team work

Joerg Denzinger, Matthias Fuchs
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: denzinge@informatik.uni-kl.de
	fuchs@informatik.uni-kl.de

Abstract
The team work method is a concept for distributing automated theorem provers and
so to activate several experts to work on a given problem. We have implemented
this for pure equational logic using the unfailing Knuth-Bendix completion
procedure as basic prover. In this paper we present three classes of experts
working in a goal oriented fashion. In general, goal oriented experts perform
their job "unfair" and so are often unable to solve a given problem alone.
However, as a team member in the team work method they perform highly efficient,
even in comparison with such respected provers as Otter 3.0 or REVEAL, as we
demonstrate by examples, some of which can only be proved using team work.

The reason for these achievements results from the fact that the team work
method forces the experts to compete for a while and then to cooperate by
exchanging their best results. This allows one to collect "good" intermediate
results and to forget "useless" ones. Completion based proof methods are
frequently regarded to have the disadvantage of being not goal oriented. We
believe that our approach overcomes this disadvantage to a large extend.

Keywords
Automated theorem proving, distributed deduction, goal oriented completion

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1994/papers/
file: Denzinger.SR-94-04.ps.Z