| |
Click here for full text:
An Explicating Theorem Prover for Quantified Formulas
Flanagan, Cormac; Joshi, Rajeev; Saxe, James B.
HPL-2004-199
Keyword(s): theorem proving; quantifiers; SAT solving; explication
Abstract: Recent 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 Verifun for quantifier-free formulas over the theories of equality, rational linear arithmetic, and arrays. In this paper, we extend our original Verifun architecture to support universal and existential quantifiers, which arise naturally in many verification domains, and we verify key correctness properties of our design.
15 Pages
Back to Index
|
Printable version
