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. (Url (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},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/C9.pdf}},
  Year =	 2000,
}
Powered by bibtexbrowser