Technical reports
Recording HOL proofs
Wai Wong
July 1993, 57 pages
DOI: 10.48456/tr-306
Abstract
This paper describes a text file format for recording HOL proofs. It is intended to become an interface between HOL and proof checkers. Modification to HOL-88 has been carried out to incorporate a proof recorder to generate a proof file in this format. The usage of this new feature is explained by a simple example. A more substantial proof has been recorded, and benchmark data is presented here.
Full text
PDF (3.8 MB)
BibTeX record
@TechReport{UCAM-CL-TR-306, author = {Wong, Wai}, title = {{Recording HOL proofs}}, year = 1993, month = jul, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-306.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-306}, number = {UCAM-CL-TR-306} }