Technical reports

Natural deduction theorem proving via higher-order resolution

Lawrence C. Paulson

May 1985, 22 pages

DOI: 10.48456/tr-67

Abstract

An experimental theorem prover is described. Like LCF it is embedded in the metalanguage ML and supports backward proof using tactics and tacticals. The prover allows a wide class of logics to be introduced using Church’s representation of quantifiers in the typed lambda-calculus. The inference rules are expressed as a set of generalized Horn clauses containing higher-order variables. Depth-first subgoaling along inference rules is essentially linear resolution, but using higher-order unification instead of first-order. This constitutes a higher-order Prolog interpreter.

The rules of Martin Löf’s Constructive Type Theory have been entered into the Prover. Special tactics inspect a goal and decide which type theory rules may be appropriate, avoiding excessive backtracking. These tactics can automatically derive the types of many Type Theory expressions. Simple functions can be derived interactively.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-67,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Natural deduction theorem proving via higher-order
         	   resolution}},
  year = 	 1985,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-67.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-67},
  number = 	 {UCAM-CL-TR-67}
}