Technical reports

Generic automatic proof tools

Lawrence C. Paulson

May 1996, 28 pages

DOI: 10.48456/tr-396

Abstract

This paper explores a synthesis between two distinct traditions in automated reasoning: resolution and interaction. In particular it discusses Isabelle, an interactive theorem prover based upon a form of resolution. It aims to demonstrate the value of proof tools that, compared with traditional resolution systems, seem absurdly limited. Isabelle’s classical reasoner searches for proofs using a tableau approach. The reasoner is generic: it accepts rules proved in applied theories, involving defined connectives. New constants are not reduced to first-order logic; the reasoner

Full text

PDF (0.2 MB)
PS (0.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-396,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Generic automatic proof tools}},
  year = 	 1996,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-396.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-396},
  number = 	 {UCAM-CL-TR-396}
}