An Explicating Theorem Prover for Quantified Formulas

[摘要] 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

[发布机构] HP Development Company

[学科分类] 计算机科学（综合）

[关键词] theorem proving;quantifiers;SAT solving;explication