An Explicating Theorem Prover for Quantified Formulas

Flanagan, Cormac ; Joshi, Rajeev ; Saxe, James B.

HP Development Company

关键词: theorem proving;    quantifiers;    SAT solving;    explication;   

RP-ID  :  HPL-2004-199

学科分类：计算机科学（综合）

美国|英语

来源: HP Labs

【 摘 要 】

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