Tactics for Hierarchical Proof

Abstract. There is something of a discontinuity at the heart of popular tactical theorem provers. Low-level, fully-checked mechanical proofs are large trees consisting of primitive logical inferences. Meanwhile, high-level human inputs are lexically structured formal texts which include tactics describing search procedures. The proof checking process maps from the high-level to low-level, but after that, explicit connections are usually lost. The lack of connection can make it difficult to understand the proof trees produced by successful tactic proofs, and difficult to debug faulty tactic proofs. We propose the use of hierarchical proofs, also known as hiproofs, to help bridge these levels. Hiproofs superimpose a labelled hierarchical nesting on ary proof tree, abstracting from the underlying logic. The labels and nesting are used to describe the organisation of the proof, typically relating to its construction process. In this paper we introduce a foundational tactic language Hitac w...

• Type: Journal
• Year: 2010
• Where: MICS
• Authors: David Aspinall, Ewen Denney, Christoph Lüth
• Keywords: MICS 2010, Semantics, Tactic Proofs, Tactical Theorem