Technical reports

Representing higher-order logic proofs in HOL

J. von Wright

January 1994, 28 pages

DOI: 10.48456/tr-323

Abstract

When using a theorem prover based on classical logic, such as HOL [2], we are generally interested in the facts that are proved (the theorems) than in the way in which they were proved (the proofs). However we may be interested in checking the correctness of the proofs. Since machine-generated proofs are generaly very long we need a computer program, a proof checker, to do this. However, we would also want the correctness of the proof checker to be verified formally. One way of doing this is by specifying it in a mechanised logic (such as that of the HOL system) and then doing a correctness proof in that logic. While this may seem circular, it is acceptable provided we have a theory of proofs embedded in the logic.

This paper describes an attempt to formalise the notion of HOL proofs within HOL. The aim is to be able to verify (inside HOL) that what is claimed to be a proof really is a proof.

Full text

PDF (1.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-323,
  author =	 {von Wright, J.},
  title = 	 {{Representing higher-order logic proofs in HOL}},
  year = 	 1994,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-323.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-323},
  number = 	 {UCAM-CL-TR-323}
}