Hierarchical Proof Structures
Ewen Denney, Konstantinos Tourlas, John Power · 2005
Abstract. Motivated by structure arising in tactic-based theorem proving, we develop the concept of hierarchical proof tree or hiproof by characterising a geometrically natural definition in terms of its family of proof views. We first recall a definition of hierarchical proof tree, explaining its axioms and illustrating by example. We then describe notions involved with proof views. Then we characterise hierarchical proof trees in terms of dags of proof views. Our ultimate goal is to axiomatise the structure required for constructing and navigating tactic-based proofs. This is work in progress towards that end. 1