Towards Proof Planning for ω+
Carsten Schürmann, Serge Autexier · Electronic Notes in Theoretical Computer Science · 2002
This paper describes the proof planning system P ω+ for the meta theorem prover for LF implemented in Twelf. The main contributions include a formal system that approximates the flow of information between assumptions and goals within a meta proof, a set of inference rules to reason about those approximations, and a soundness proof that guarantees that the proof planner does not reject promising proof states. Proof planning in P ω+ is decidable.