What is Proof Planning?

Overview

There are three main proof planning systems: The Clam series, Omega and IsaPlanner all of which implement proof planning slightly differently and all of which use slightly varying terminology. Moreover all, so far, have had only small user communities. I believe the proof uptake is related to the difficulty involved in customising these systems unless you happen to be a developer. There is also a lack of clarity about the nature of proof planning and the benefits it might offer over other automated reasoning techniques and systems.

I personally believe that the advantage of proof planning is that it can be viewed as a generic hierarchical framework for developing automation techniques. It therefore has applications as a kind of scripting language for on-the-fly construction of automation and the prototyping of techniques for later implementation within separate systems; for providing tools for user development of automated reasoning within interactive systems; and the cognitive modeling of reasoning.

Within this theme I have several sub-interests:

What is Proof Planning?: This is joint work with Dr. Martin Pollet and Dr. Mateja Jamnik (Cambridge) to both describe the key concepts involved in proof planning and compare the existing systems. Out of this has arisen work on the equivalence of different proof search control methodologies which has applications to interactive theorem proving as well as proof planning.
Lightweight Proof Planning: I'm interested in the extent to which lightweight proof-planning can be grafted onto existing theorem proving systems. How much support is needed to allow how much functionality? how difficult it is to implement different aspects of proof planning within a standard theorem prover? and how much value can you obtain from which features?
Proof Planning Strategy Development Languages: Work with Dr. Jeremy Gow (UCL Interaction Centre) and Dr. Lucas Dixon (Edinburgh) on developing a unified user language which can be used to customise proof planning systems. Our ideal is that this should be a system independent language which could be compiled down to any particular proof planning implementation.

People

Funding

EPSRC grant GR/S01771/01: The Integration and Interaction of Multiple Mathematical Reasoning Processes.

Publications

L. A. Dennis, M. Jamnik and M. Pollet. On the Comparison of Proof Planning Systems: Lambda-Clam, Omega and IsaPlanner. 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005), Electronic Notes in Computer Science (ENTCS) 151. pp. 93-110, 2006. BibTex
An Architecture for Proof Planning Systems, in L. P. Kaelbling and A. Saffoitti (Eds): Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI-05, IJCAI, Inc. pp. 1558-1559, 2005. BibTex.
Louise Dennis, Proof Planning Methods in OMDoc, Edinburgh Dream Group Blue Book Note 1346.
Louise Dennis, What is the Difference between a Method and a Tactic?, Edinburgh Dream Group Blue Book Note 1356.
Louise Dennis, What is the Difference between a Method and a Tactic II, straying into What is Proof Planning and Why do we do it?, Edinburgh Dream Group Blue Book Note 1381.
Louise Dennis, Everything is a Critic, Edinburgh Dream Group Blue Book Note 1492.
Louise Dennis, Lucas Dixon and Jeremy Gow, A Proof Plan Specification Language, Edinburgh Dream Group Blue Book Note 1631.

Code

HOL Code for Control Rules: control_rules.sml, creuclidScript.sml

Bibliography

Bundy, 91: A. Bundy, A Science of Reasoning, in J.-L. Lassez and G. Plotkin (eds), Computational Logic: Essays in Honor of Alan Robinson, pp. 178-198, MIT Press, 1991.