Capturing Hiproofs in HOL Light

Steven Obua, Mark Adams, David Aspinall

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular portions to explain their purpose. In this paper we present two complementary methods for capturing hiproofs in HOL Light, along with a tool to produce web-based visualisations. The first method uses tactic recording, by modifying tactics to record their arguments and construct a hierarchical tree; this allows a tactic proof script to be modified. The second method uses proof recording, which extends the HOL Light kernel to record hierachical proof trees alongside theorems. This method is less invasive, but requires care to manage the size of the recorded objects. We have implemented both methods, resulting in two systems: Tactician and HipCam.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationProceedings MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-642-39320-4
ISBN (Print)978-3-642-39319-8
Publication statusPublished - 2013


Dive into the research topics of 'Capturing Hiproofs in HOL Light'. Together they form a unique fingerprint.

Cite this