Department of Computer Science and Technology

Technical reports

A proof checked for HOL

Wai Wong

March 1996, 165 pages

DOIhttps://doi.org/10.48456/tr-389

Abstract

Formal proofs generated mechanically by theorem provers are often vary large and shallow, and the theorem provers themselves very complex. Therefore, in certain application areas, such as safety-critical systems, it is necessary to have an independent means for ensuring the consistency of such formal proofs. This report describes an efficient proof checker for the HOL theorem prover. This proof checker has been tested with practical proofs consisting of thousands of inference steps. It was implemented in Standard ML of New Jersey.

The first part of the report gives an overview of the program. It describes: the rationale of developing a proof checker; how to use the checker; and, how the checker works.

The second part of the report describes the program in detail. The complete source code is included in the description.

Full text

PDF (11.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-389,
  author =	 {Wong, Wai},
  title = 	 {{A proof checked for HOL}},
  year = 	 1996,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-389.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-389},
  number = 	 {UCAM-CL-TR-389}
}