Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #949
Title:	Proof Planning Methods as Schemas
Authors:	Bundy,A; Richardson,J
Date:	Apr 1999
Presented:	Submitted to the Journal of Symbolic Computation
Keywords:
Abstract:	A major problem in automated theorem proving is search control. Fully expanded proofs are generally built from a large number of relatively low-level inference steps, with the result that searching the space of possible proofs at this level is very expensive.Proof planning is a technique by which common proof techniques are encoded as schemas, which we call methods. Proof built using methods tend to be short, because the methods encode relatively long sequences of inference steps, and to be understandable, because the user can recognise the mathematical techniques being applied. Proof critics exploit the high-level nature of proof plans to patch failed proof attempts.A mapping from proof planning methods and proof construction tactics provides a link between the proof planning meta-level and fully expansive (object-level) proofs.Extensive experiments with proof planning reveal that a knowledge-based approach to automating proof construction works, and has useful properties.
Download:	POSTSCRIPT COPY

Division of InformaticsForrest Hill & 80 South Bridge