Technical reports

Simplification with renaming:
a general proof technique for tableau and sequent-based provers

Fabio Massacci

May 1997, 26 pages

DOI: 10.48456/tr-424

Abstract

Tableau and sequent calculi are the basis for most popular interactive theorem provers for hardware and software verification.

Yet, when it comes to decision procedures or automatic proof search, tableaux are orders of magnitude slower than Davis-Putnam, SAT based procedures or other techniques based on resolution.

To meet this challenge, this paper proposes a theoretical innovation: the rule of simplification, which plays the same role for tableaux as subsumption does for resolution, and unit for Davis-Putman.

This technique gives a unifying view of a number of tableaux-like calculi such as DPLL, KE, HARP, hyper-tableaux etc. For instance the stand-alone nature of the first-order Davis-Putnam-Longeman-Loveland procedure can be explained away as a case of Smullyan tableau with propositional simplification.

Besides its computational effectiveness, the simplicity and generality of simplification make its extension possible in a uniform way. We define it for propositional and first order logic and a wide range of modal logics. For a full-fledged first order simplification we combine it with another technique, renaming, which subsumes the use of free universal variables in sequent and tableau calculi.

New experimental results are given for random SAT and the IFIP benchmarks for hardware verification.

Full text

DVI (0.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-424,
  author =	 {Massacci, Fabio},
  title = 	 {{Simplification with renaming: a general proof technique
         	   for tableau and sequent-based provers}},
  year = 	 1997,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-424.dvi.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-424},
  number = 	 {UCAM-CL-TR-424}
}