A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover
Lazy proof explication is a theorem-proving architecture that allows a combination of Nelson-Oppen-style decision procedures to leverage a SAT solver’s ability to perform propositional reasoning efficiently. The SAT solver finds ways to satisfy a given formula propositionally, while the various decision procedures perform theory reasoning to block propositionally satisfied instances that are not consistent with the theories. Supporting quantifiers in this architecture poses a challenge as quantifier instantiations can dynamically introduce boolean structure in the formula, requiring a tighter interleaving between propositional and theory reasoning.
This paper proposes handling quantifiers by using two SAT solvers, thereby separating the propositional reasoning of the input formula from that of the instantiated formulas. This technique can then reduce the propositional search space, as the paper demonstrates. The technique can use off-the-shelf SAT solvers and requires only that the theories are checkpointable.
KeywordsDecision Procedure Theorem Prover Theory Reasoning Satisfying Assignment Original Formula
- 3.de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002 (May 2002)Google Scholar
- 4.Déharbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Proc. of the International Conference on Software Engineering and Formal Methods (SEFM 2003), Camberra, Australia (September 2003)Google Scholar
- 5.Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (July 2003)Google Scholar
- 6.Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)Google Scholar
- 8.Flanagan, C., Joshi, R., Saxe, J.B.: An explicating theorem prover for quantified formulas. Technical Report HPL-2004-199, HP Labs (2004)Google Scholar
- 9.Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)CrossRefGoogle Scholar
- 11.Nelson, C.G.: Techniques for Program Verification. PhD thesis, Stanford University, 1980. Also available as Xerox PARC technical report CSL-81-10 (1981)Google Scholar
- 14.Zhang, L., Malik, S.: Extracting small unsatisfiable cores from unsatisfiable boolean formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2003)Google Scholar