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.
展开▼
