Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus
Cooperation in Heterogeneous Theorem Prover Networks
Project Goals:
Even for one particular logic, as for example first-order logic with equality,
there are many different calculi and for each calculus several theorem prover
that employ this calculus. Even more, often there a specialized calculi and
provers for some parts of the logic, as for example equality. Clearly, a
potential user without much background about calculi and provers is overwhelmed
by the multitude of provers he is offered and at quite a loss. Also, very often
an empirical comparision will show that each calculus and each of its provers
will have their top results and their weaknesses (see for example the
CADE-13 Theorem Prover Competition)
Many people suggested to combine several provers into a kind of "super"-prover,
but there are major problems involved, as for example:
control of this "super"-prover
major changes in each prover (even a reimplementation may be necessary)
each prover has to be modeled in each other prover to deligate appropriate
tasks
the integration of a new prover is very hard
Therefore we propose in this project an agent- oriented, loosely coupled
approach for achieving cooperation between already existing theorem provers.
This approach (in its first version) requires only small changes in the provers that are mainly the ability to periodically write new results generated by
the prover into a file and the ability to periodically read new results from several files (and, of course, integrate these results into the own proving process). In order to protect a prover from large amounts of data from other provers, referees filter most of the data out and only let very promising data pass between the provers (for an explanation of the referee concept see our pages about the teamwork method ).
Partners:
Humboldt-Universität Berlin
Funding:
Deutsche Forschungsgemeinschaft, Schwerpunktprogramm "Deduktion"