Towards Learning New Methods in Proof Planning (bibtex)

by Mateja Jamnik, Manfred Kerber, Christoph Benzmüller

Abstract:

In this paper we propose how proof planning systems can be extended by an automated learning capability. The idea is that a proof planner would be capable of learning new proof methods from well chosen examples of proofs which use a similar reasoning strategy to prove related theorems, and this strategy could be characterised as a proof method. We propose a representation framework for methods, and a machine learning technique which can learn methods using this representation framework. The technique can be applied (amongst other) to learn whether and when to call external systems such as theorem provers or computer algebra systems. This is work in progress, and we hope to gain useful feedback from the CALCULEMUS community.

Reference:

Towards Learning New Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Christoph Benzmüller), In Symbolic Computation and Automated Reasoning (Manfred Kerber, Michael Kohlhase, eds.), A.K.Peters, pp. 142-159, 2000. (Preprint: http://christoph-benzmueller.de/papers/C9.pdf)

Bibtex Entry:

@inproceedings{C9, Abstract = {In this paper we propose how proof planning systems can be extended by an automated learning capability. The idea is that a proof planner would be capable of learning new proof methods from well chosen examples of proofs which use a similar reasoning strategy to prove related theorems, and this strategy could be characterised as a proof method. We propose a representation framework for methods, and a machine learning technique which can learn methods using this representation framework. The technique can be applied (amongst other) to learn whether and when to call external systems such as theorem provers or computer algebra systems. This is work in progress, and we hope to gain useful feedback from the CALCULEMUS community.}, Author = {Mateja Jamnik and Manfred Kerber and Christoph Benzm{\"u}ller}, Booktitle = {Symbolic Computation and Automated Reasoning}, Editor = {Manfred Kerber and Michael Kohlhase}, Keywords = {own, CALCULEMUS, Symb. Computation and Symb. Reasoning, Proof Planning, Machine Learning}, Pages = {142-159}, Publisher = {A.K.Peters}, Title = {Towards Learning New Methods in Proof Planning}, Addendum = {Preprint: \url{http://christoph-benzmueller.de/papers/C9.pdf}}, Year = 2000, }