Technical reports

HOL
A machine oriented formulation of higher order logic

Mike Gordon

July 1985, 52 pages

DOI: 10.48456/tr-68

Abstract

In this paper we describe a formal language intended as a basis for hardware specification and verification. The language is not new; the only originality in what follows lies in the presentation of the details. Considerable effort has gone into making the formalism suitable for manipulation by computer.

The logic described here underlies an automated proof generator called HOL. The HOL logic is derived from Church’s Simple Type Theory by: making the syntax more readable, allowing types to contain variables, and building in the Axiom of Choice via Hilbert’s ε-operator.

The exact syntax of the logic is defined relative to a theory, which determines the types and constants that are available. Theories are developed incrementally starting from the standard theories of truth-values or booleans, and of individuals. This paper describes the logic underlying the HOL system.

Full text

PDF (1.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-68,
  author =	 {Gordon, Mike},
  title = 	 {{HOL : A machine oriented formulation of higher order logic}},
  year = 	 1985,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-68.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-68},
  number = 	 {UCAM-CL-TR-68}
}