SMELS: Satisfiability Modulo Equality with Lazy Superposition
We give a method for extending efficient SMT solvers to handle quantifiers, using Superposition inference rules. In our method, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SMT solver, which runs a DPLL method to build partial models. The partial model is passed to a Congruence Closure procedure, as is normally done in SMT. Congruence Closure calculates all reduced (dis)equations in the partial model and passes them to a Superposition procedure, along with a justification. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the (dis)equations and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of this method, using a nontrivial modification of Bachmair and Ganzinger’s model generation technique. We believe this combination uses the best of both worlds, an SMT process to handle ground clauses efficiently, and a Superposition procedure which uses orderings to handle the nonground clauses.
KeywordsInference System Inference Rule Truth Assignment Ground Instance Linear Arithmetic
Unable to display preview. Download preview PDF.
- 1.The Yices SMT Solver, http://yices.csl.sri.com/tool-paper.pdf
- 4.Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 462–476. Springer, Heidelberg (1992)Google Scholar
- 9.Déharbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Press, I.C.S. (ed.) Proc. of the Int. Conf. on Software Engineering and Formal Methods (SEFM 2003) (2003)Google Scholar
- 10.Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems, Handbook of Theoretical Computer Science, ch. 6, vol. B, pp. 244–320 (1990)Google Scholar
- 11.Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148, HP Laboratories (2003)Google Scholar
- 14.Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Hand. of Automated Reasoning. Elsevier and MIT Press (2001)Google Scholar