Computer Laboratory

Technical reports

Designing a theorem prover

Lawrence C. Paulson

May 1990, 57 pages

Abstract

The methods and principles of theorem prover design are presented through an extended example. Starting with a sequent calculus for first-order logic, an automatic prover (called Folderol) is developed. Folderol can prove quite a few complicated theorems, although its search strategy is crude and limited. Folderol is coded in Standard ML and consists largely of pure functions. Its complete listing is included.

The report concludes with a survey of other research in theorem proving: the Boyer/Moore theorem prover, Automath, LCF, and Isabelle.

Full text

PDF (0.3 MB)
DVI (0.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-192,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Designing a theorem prover}},
  year = 	 1990,
  month = 	 may,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-192.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-192}
}