Tactics for Hierarchical Proof

David Aspinall, Ewen Denney, Christoph Lüth

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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 an ordinary 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 which constructs hiproofs in a generic setting. Hitac programs can be evaluated using a big-step or a small-step operational semantics. The big-step semantics captures the intended meaning, whereas the small-step semantics is closer to possible implementations and provides a unified notion of proof state. We prove that the semantics are equivalent and construct valid proofs. We also explain how to detect terms which are stuck in the small-step semantics, and how these suggest interaction points with debugging tools. Finally we show some typical examples of tactics, constructed using tactical combinators, in our language.
Original languageEnglish
Pages (from-to)309-330
Number of pages22
JournalMathematics in Computer Science
Volume3
Issue number3
DOIs
Publication statusPublished - May 2010

Keywords / Materials (for Non-textual outputs)

  • Hierarchical proof
  • Hiproof
  • Tactical theorem proving

Fingerprint

Dive into the research topics of 'Tactics for Hierarchical Proof'. Together they form a unique fingerprint.

Cite this