Planning diagonalization proofs

Abstract

Proof planning [Bun91] is the search for a sequence of tactics (a proof plan)which can be applied to construct an object level proof. The used operators (methods) are specifications of tactics represented in a meta-language. A method specifies when the associated tactic can be applied and what its effects are. In our approach, we extend methods that represent well-known proof techniques, such as induction or diagonalization, with control knowledge and call them strategies.