Continuations of Proof Strategies

Julian Richardson and Alan Smaill
Edinburgh, UK

Abstract (Introduction)

Proof planning \cite{jrjrpub413} is a technique for automatically
constructing proofs from abstractions of tactics called {\em
methods}. Proof planning has been successfully applied in many
domains, for example: mathematical induction \cite{jrjrpub413},
higher-order program synthesis \cite{jrjrLRS00} and hardware
verification \cite{jrjrpub828}. In the first proof planner, \jrjrclam\
\cite{jrjrpub507}, application of methods during the search for a
proof plan was controlled by a simple waterfall
(\S\ref{waterfall}). In this paper, we describe {\em methodical}
expressions, which we use to define more complex proof search
strategies. Methodicals compose methods in the same way that tacticals
compose tactics. The work described in this paper has been implemented
as part of the \jrjrlclam\ system
\cite{jrjrrichardson+98,jrjrlclam-man ual}.

We present a meta-interpreter which gives a semantics to methodical
expressions. In conjunction with a mechanism for executing methods and
a search strategy, this meta-interpreter can be used as a proof
planner. This planner does not have any notion of proof state, and is
unsuitable for interactive proof. 

We present a set of transformation rules which we use to define a new
meta-interpreter which does maintain a notion of proof state, is
suitable for interactive proof, and we prove that it is equivalent to
the first in the sense that it produces the same plans. This
meta-interpreter has been used for some time as the basis of the
interactive planner in \jrjrlclam, although it does not yet treat the
whole of the methodical language.

The transformation rules can be interpreted as defining a notion of
{\em continuation} \cite{jrjrcontinuation-summary} for proof
strategies. Previous work on a continuation semantics for Prolog
\cite{jrjradeb} indicates how the meta-interpreter should be extended
to cover the more problematical elements of the methodical language. 

The definition of methodicals, use of formal proof to verify
equivalence of proof planners, and use of continuations in the context
of proof planning are novel.