Department of Computer Science and Technology

Technical reports

Recording HOL proofs

Wai Wong

July 1993, 57 pages

DOIhttps://doi.org/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}
}