Technical reports

A generic tableau prover and its integration with Isabelle

Lawrence C. Paulson

January 1998, 16 pages

DOI: 10.48456/tr-441

Abstract

A generic tableau prover has been implemented and integrated with Isabelle. It is based on leantap but is much more complicated, with numerous modifications to allow it to reason with any supplied set of tableau rules. It has a higher-order syntax in order to support the binding operators of set theory; unification is first-order (extended for bound variables in obvious ways) instead of higher-order, for simplicity.

When a proof is found, it is returned to Isabelle as a list of tactics. Because Isabelle verifies the proof, the prover can cut corners for efficiency’s sake without compromising soundness. For example, it knows almost nothing about types.

Full text

PDF (0.2 MB)
PS (0.1 MB)
DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-441,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{A generic tableau prover and its integration with Isabelle}},
  year = 	 1998,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-441.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-441},
  number = 	 {UCAM-CL-TR-441}
}