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.
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.
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.
