Technical reports

# Designing a theorem prover

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

## 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} }