Research Group 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:
• Learning of knowledge (learning phase):
• What or whom do we learn from?
• What to learn?
• How to represent and store the learned knowledge?
• What learning method to use?
• Using the learned knowledge (application phase):
• How to detect applicable knowledge?
• How to apply knowledge?
• How to detect and deal with (applicable, but) misleading knowledge?
• How to combine knowledge from different sources?
• General machine learning problem:
• Which concepts of similarity are helpful?
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.

Funding:
Deutsche Forschungsgemeinschaft, Schwerpunktprogramm "Deduktion"

## Publications:

• Fuchs, M. : Exploiting past proof Experience, LSA-Report LSA-95-08E, University of Kaiserslautern, 1995.
• Fuchs, M. : Learning proof heuristics by adapting parameters, Proc. 12th ML, Morgan Kaufmann, 1995, pp. 235-243.
Also as SEKI-Report SR-95-02, University of Kaiserslautern, 1995.
• Fuchs, M. : Experiments in the Heuristic Use of Past Proof Experience, Proc. Proc. CADE-13, New Brunswick, LNAI 1104, 1996, pp. 523-537.
Also as SEKI-Report SR-95-10, University of Kaiserslautern, 1995.
• Denzinger, J.; Schulz, S. : Learning Domain Knowledge to Improve Theorem Proving, Proc. CADE-13, New Brunswick, LNAI 1104, 1996, pp. 62-76.
• Fuchs, M. : Towards Full Automation of Deduction: A Case Study, SEKI-Report SR-96-07, University of Kaiserslautern, 1996.
• Fuchs, Matt.: Evolving Combinators, Proc. CADE-97, Townsville, LNAI 1249, 1997, pp. 416-430.
Extended version as SEKI-Report SR-96-08, University of Kaiserslautern, 1996.
• Denzinger, J. ; Fuchs, Matt. ; Fuchs, Marc: High Performance ATP Systems by Combining Several AI Methods, Proc. IJCAI-97, Morgan Kaufmann, 1997, pp. 102-107.
Extended version as SEKI-Report SR-96-09, University of Kaiserslautern, 1996.