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:
- What or whom do we learn from?
- What do we learn?
- How do we represent and store the learned knowledge?
- Using the learned knowledge:
- How do we detect applicable knowledge?
- How do we apply knowledge?
- How do we detect and deal with (applicable, but) misleading knowledge?
- How do we combine knowledge from different sources?
Clearly the answers to the questions depend from 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.
Download full paper (76 Kbytes)
- 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, M. : Evolving Combinators,
SEKI-Report SR-96-08, University of Kaiserslautern, 1996.
- Denzinger, J. ; Fuchs, Matt. ; Fuchs, Marc: High Performance ATP
Systems by Combining Several AI Methods, SEKI-Report SR-96-09,
University of Kaiserslautern, 1996.
Persons Involved:
Links of Interest:
If you have questions, problems or suggestions send email to
denzinge@informatik.uni-kl.de