In this article we present a mechanism for recording HOL Light tactic proofs in a hierarchical tree structure, with information stored at the level of atoms in the user’s ML proof script. This is written to support refactoring of tactic proofs, so that single-tactic packaged-up proofs can be flattened to a series of interactive tactic steps, and vice versa. It also provides a good basis for proof visualisation and for proof querying capability. The techniques presented can be adapted straightforwardly to other systems.
|Title of host publication||Proceedings of the IJCAR workshop on Automated Theory Exploration|
|Number of pages||6|
|Publication status||Published - Jun 2012|