TY - JOUR
T1 - Hiproofs: A Hierarchical Notion of Proof Tree
AU - Denney, Ewen
AU - Power, John
AU - Tourlas, Konstantinos
PY - 2006/5/12
Y1 - 2006/5/12
N2 - Motivated by the concerns of theorem-proving, we generalise the notion of proof tree to that of hierarchical proof tree. Hierarchical trees extend ordinary trees by adding partial order structure to the set of nodes: that allows us to visualise a node as a rectangle in the plane rather than as a point, letting us use the containment relation to express structure additional to that given by a tree. A hierarchical proof tree, or hiproof for short, is a hierarchical tree with nodes labelled by tactics. We motivate the details of our definition by reference to the behaviour of tactics in tactical theorem proving. We characterise the construction of the ordinary proof tree underlying a hierarchical proof tree as a left adjoint. We then analyse the notion of proof refinement with respect to hierarchy, and we give a characterisation of previous termhiproofs that is more directly suited to implementation.
AB - Motivated by the concerns of theorem-proving, we generalise the notion of proof tree to that of hierarchical proof tree. Hierarchical trees extend ordinary trees by adding partial order structure to the set of nodes: that allows us to visualise a node as a rectangle in the plane rather than as a point, letting us use the containment relation to express structure additional to that given by a tree. A hierarchical proof tree, or hiproof for short, is a hierarchical tree with nodes labelled by tactics. We motivate the details of our definition by reference to the behaviour of tactics in tactical theorem proving. We characterise the construction of the ordinary proof tree underlying a hierarchical proof tree as a left adjoint. We then analyse the notion of proof refinement with respect to hierarchy, and we give a characterisation of previous termhiproofs that is more directly suited to implementation.
UR - http://dx.doi.org/10.1016/j.entcs.2005.11.063
U2 - 10.1016/j.entcs.2005.11.063
DO - 10.1016/j.entcs.2005.11.063
M3 - Article
SN - 1571-0661
VL - 155
SP - 341
EP - 359
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -