A Semantics for Proof Plans with Applications to
		       Interactive Proof Planning

			   Julian Richardson
			  julianr@cee.hw.ac.uk

To be published by Springer Verlag in Proceedings of 9th
International Conference on Logic for Programming Artificial
Intelligence and Reasoning (LPAR 2002), October 14-18th,
2002, Tbilisi, Georgia.

Abstract

Proof planning is an automated theorem proving technique
which encodes meaningful blocks of proof as planning
operators called methods. Methods often encode complex
control strategies, and a language of methodicals, similar
to tacticals, has been developed to allow methods to be
expressed in a modular way.

Previous work has demonstrated that proof planning can be
effective for interactive theorem proving, but it has not
been clear how to reconcile the complex control encoded by
methodicals with the needs of interactive theorem proving.

In this paper we develop an operational semantics for
methodicals which allows reasoning about proof plans in the
abstract, without generating object-level proofs, and
facilitates interactive planning. The semantics is defined
by a handful of deterministic transition rules, represents
disjunction and backtracking in the planning process
explicitly, and handles the cut methodical correctly.