Abstract
Applications in software verification often require determining the satisfiability of first-order formulæ with respect to some background theories. During development, conjectures are usually false. Therefore, it is desirable to have a theorem prover that terminates on satisfiable instances. Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrated theory reasoning. Superposition-based inference systems are strong at reasoning with equalities, universally quantified variables, and Horn clauses. We describe a calculus that tightly integrates Superposition and SMT solvers. The combination is refutationally complete if background theory symbols only occur in ground formulæ, and non-ground clauses are variable inactive. Termination is enforced by introducing additional axioms as hypotheses. The calculus detects any unsoundness introduced by these axioms and recovers from it.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM TOCL 10(1), 129–179 (2009)
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)
Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM TOCL 8(1), 180–208 (2007)
Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proc. 4th PDPAR Workshop, FLoC 2006. ENTCS, vol. 174(8), pp. 55–70. Elsevier, Amsterdam (2007)
Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T-satisfiability procedures. J. Logic and Comput. 18(1), 77–96 (2008)
Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput., 1–42 (to appear)
Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 513–527. Springer, Heidelberg (2006)
Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Kluwer Academic Publishers, Amsterdam (2004)
Cantone, D., Zarba, C.G.: A decision procedure for monotone functions over bounded and complete lattices. In: de Swart, H. (ed.) TARSKI 2006. LNCS (LNAI), vol. 4342, pp. 318–333. Springer, Heidelberg (2006)
de Moura, L., Bjørner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475–490. Springer, Heidelberg (2008)
de Moura, L., Bjørner, N.: Model-based theory combination. In: Krstić, S., Oliveras, A. (eds.) Proc. 5th SMT Workshop, CAV 2007. ENTCS, vol. 198(2), pp. 35–50. Elsevier, Amsterdam (2008)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. PLDI, pp. 234–245 (2002)
Gallier, J., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. J. ACM 40(1), 1–16 (1993)
Halpern, J.Y.: Presburger Arithmetic with unary predicates is \(\Pi_1^1\) Complete. J. Symb. Logic 56, 637–642 (1991)
Jacobs, S.: Incremental instance generation in local reasoning. In: Notes 1st CEDAR Workshop, IJCAR 2008, pp. 47–62 (2008)
Lynch, C.A.: Unsound theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 473–487. Springer, Heidelberg (2004)
MacNeille, H.M.: Partially ordered sets. Transactions of the American Mathematical Society 42, 416–460 (1937)
McCune, W.W.: Otter 3.3 reference manual. Technical Report ANL/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne, IL, USA (2003)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245–257 (1979)
Snyder, W.: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. J. Symb. Comput. (1992)
Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonacina, M.P., Lynch, C., de Moura, L. (2009). On Deciding Satisfiability by DPLL(\(\Gamma+{\mathcal T}\)) and Unsound Theorem Proving. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-02959-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02958-5
Online ISBN: 978-3-642-02959-2
eBook Packages: Computer ScienceComputer Science (R0)