An Explicating Theorem Prover for Quantified Formulas
Cormac Flanagan, Rajeev Joshi, James B. Saxe · 2004
, James B. Saxe Intelligent Enterprise Technologies Laboratory HP Laboratories Palo Alto HPL-2004-199 November 2, 2004* theorem proving, quantifiers, SAT solving, explicationRecent developments in fast propositional satisfiability solvers and proof-generating decision procedures have inspired new variations on the traditional Nelson-Oppen style of theorem provers. In an earlier paper, we described the design and performance of our explicating theorem prover