Hiproofs: A Hierarchical Notion of Proof Tree

Ewen Denney, John Power, Konstantinos Tourlas

Research output: Contribution to journalArticle

16 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)341-359
Number of pages19
JournalElectronic Notes in Theoretical Computer Science
Volume155
DOIs
Publication statusPublished - 12 May 2006

Fingerprint

Theorem proving
Theorem Proving
Vertex of a graph
Partial Order
Rectangle
Refinement
Express
Generalise

Cite this

Hiproofs: A Hierarchical Notion of Proof Tree. / Denney, Ewen; Power, John; Tourlas, Konstantinos.

In: Electronic Notes in Theoretical Computer Science, Vol. 155, 12.05.2006, p. 341-359.

Research output: Contribution to journalArticle

Denney, Ewen ; Power, John ; Tourlas, Konstantinos. / Hiproofs: A Hierarchical Notion of Proof Tree. In: Electronic Notes in Theoretical Computer Science. 2006 ; Vol. 155. pp. 341-359.
@article{ede9776031274b3683485fb83442e0b4,
title = "Hiproofs: A Hierarchical Notion of Proof Tree",
abstract = "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.",
author = "Ewen Denney and John Power and Konstantinos Tourlas",
year = "2006",
month = "5",
day = "12",
doi = "10.1016/j.entcs.2005.11.063",
language = "English",
volume = "155",
pages = "341--359",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",

}

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

VL - 155

SP - 341

EP - 359

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -