Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

 FB Inf

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: 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"

Persons Involved:

Kaiserslautern:
Berlin:

Links of Interest:

Impressum AG Formale Methoden und Deduktion Fachbereich Informatik Technische Universität Kaiserslautern Valid HTML 4.01!
Letzte Änderung: Wednesday, 26-Oct-05 08:59:20 GMT
www-aven@informatik.uni-kl.de