Towards learning new methods in proof planning
Mateja Jamnik, Manfred Kerber, Christoph Benzmüller · 2001
. 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. This is work in progress, and we hope to gain useful feedback from the workshop community. 1 Introduction Proof planning [2] is an approach to theorem proving which uses proof methods rather than low level logical inference rules to prove a theorem at hand. A proof method species and encodes a general reasoning strategy that can be used in a proof, and hence represents a number of individual inference rules. For example, an induction strategy can be encoded as a proof method. Proof planners search ...