Jump to content United States-English
HP.com Home Products and Services Support and Drivers Solutions How to Buy
» Contact HP

HP.com home

Technical Reports


HP Labs

» Research
» News and events
» Technical reports
» About HP Labs
» Careers @ HP Labs
» People
» Worldwide sites
» Downloads
Content starts here

Click here for full text: PDF

An Explicating Theorem Prover for Quantified Formulas

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


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

»Technical Reports

» 2009
» 2008
» 2007
» 2006
» 2005
» 2004
» 2003
» 2002
» 2001
» 2000
» 1990 - 1999

Heritage Technical Reports

» Compaq & DEC Technical Reports
» Tandem Technical Reports
Printable version
Privacy statement Using this site means you accept its terms Feedback to HP Labs
© 2009 Hewlett-Packard Development Company, L.P.