Recording and Refactoring HOL Light Tactic
Proofs

Mark Adams; David Aspinall

Recording and Refactoring HOL Light Tactic Proofs

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Proceedings of the IJCAR workshop on Automated Theory Exploration
Number of pages	6
Publication status	Published - Jun 2012

Access to Document

atx2012_submission_9Accepted author manuscript, 72.2 KB

Cite this

@inproceedings{259d5f74b71449169343a2783c104341,

title = "Recording and Refactoring HOL Light Tactic Proofs",

abstract = "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{\textquoteright}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. ",

author = "Mark Adams and David Aspinall",

year = "2012",

month = jun,

language = "English",

booktitle = "Proceedings of the IJCAR workshop on Automated Theory Exploration",

}

TY - GEN

T1 - Recording and Refactoring HOL Light Tactic Proofs

AU - Adams, Mark

AU - Aspinall, David

PY - 2012/6

Y1 - 2012/6

N2 - 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.

AB - 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.

M3 - Conference contribution

BT - Proceedings of the IJCAR workshop on Automated Theory Exploration

ER -

Recording and Refactoring HOL Light Tactic Proofs

Abstract

Access to Document

Fingerprint

Cite this