Abstract: Tactician is a tool for refactoring tactic proof scripts for the HOL Light theorem prover. Its core operations are packaging up a series of tactic steps into a compact proof with tactical connectives, and the reverse operation of unravelling compact proofs into interactive steps. This can be useful for novices learning from legacy proof scripts, as well as for experienced users maintaining their proofs. In this paper, we give an overview of Tactician's core capabilities and provide insight into how it is implemented.
Download PDF: tactician_hofm2015.pdf
Reference: M.Adams. Refactoring Proofs with Tactician. In Revised Selected Papers of the Colocated Workshops of the 13th International Conference on Software Engineering and Formal Methods, Volume 9509 of Lecture Notes in Computer Science, pages 53-67. Springer, 2015.