Distributing equational theorem proving

J. Avenhaus , J. Denzinger
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, 6750 Kaiserslautern, GERMANY
E-mail: {avenhaus , denzinge}@informatik.uni-kl.de

Abstract
In this paper we show that distributing the theorem proving task to several
experts is a promising idea. We describe the team work method which allows the
experts to compete for a while and then to cooperate. In the cooperation phase
the best results derived in the competition phase are collected and the less
important results are forgotten. We describe some useful experts and explain in
detail how they work together. We establish fairness criteria and so prove the
distributed system to be both, complete and correct. We have implemented our
system and show by non-trivial examples that drastical time speed-ups are
possible for a cooperating team of experts compared to the time needed by the
best expert in the team.

Keywords
distributed theorem proving, cooperation, competition, synergetic effects

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1993/papers/
file: Avenhaus.SR-93-06.SEKI.ps.Z