Automatic Learning of Proof Methods in Proof Planning

摘要

We present a framework for automated learning within mathematical reasoning systems. In particular, this framework enables proof planning systems to automatically learn new proof methods from well chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our framework consists of a representation formalism for methods and a machine learning technique which can learn methods using this representation formalism. We briefly present how to learn methods in the OMEGA proof planner. The approach is a two-stage one, first to learn method outlines and second to build complete methods from method outlines.