Capturing hiproofs in HOL light

DOI10.1007/978-3-642-39320-4_12zbMATH Open1390.68583arXiv1307.2713OpenAlexW1842581062MaRDI QIDQ2843014FDOQ2843014

Authors: Steven Obua, Mark Adams, D. Aspinall

Publication date: 9 August 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1307.2713

Recommendations

Mathematics Subject Classification ID

Cited In (6)

Uses Software

This page was built for publication: Capturing hiproofs in HOL light

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843014)