Technical reports
Generic automatic proof tools
May 1996, 28 pages
| DOI | https://doi.org/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
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}
}