Research Group Logo CS Dept.
Formal Methods and Deduction
Prof. Dr. J. Avenhaus

Learning of Search Heuristics for Theorem Proving

Project Goals:

An important aspect of an automated theorem prover with respect to its success is its control of its inference rules. If the control is not able to choose enough inferences leading to a proof out of a ever growing number of candidates, the best implementation and the most improved calculus are not enough to prove hard problems. Mathematicians have the same problem but deal with it very well. One of the main differences between a mathematician and most of todays automated theorem provers is the amount of learned (control) knowledge a mathematician has and is able to make good use of.

Naturally, the control knowledge a theorem prover needs and the use it makes of it is quite different from the mathematician's way, but learning from successful proofs is definitely a good way to improve the control of a prover. But learning is not enough to improve the performance of the prover. Basically, the following problems have to be solved: Clearly the answers to the questions depend on each other and there are several possible (and usable) answers. We use as basis a distributed prover based on the teamwork method . This takes care of several of the problems on the application side of knowledge. First concepts for the other problems can be found in our publications.

Deutsche Forschungsgemeinschaft, Schwerpunktprogramm "Deduktion"


Persons Involved:

Links of Interest:

Impressum RG Formal Methods and Deduction Department of Informatics Technical University of Kaiserslautern Valid HTML 4.01!

Last Update: Wednesday, 26-Oct-05 08:59:21 GMT