Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Theory Combination: Beyond Equality Sharing

  • Chapter
  • First Online:
Description Logic, Theory Combination, and All That

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11560))

Abstract

Satisfiability is the problem of deciding whether a formula has a model. Although it is not even semidecidable in first-order logic, it is decidable in some first-order theories or fragments thereof (e.g., the quantifier-free fragment). Satisfiability modulo a theory is the problem of determining whether a quantifier-free formula admits a model that is a model of a given theory. If the formula mixes theories, the considered theory is their union, and combination of theories is the problem of combining decision procedures for the individual theories to get one for their union. A standard solution is the equality-sharing method by Nelson and Oppen, which requires the theories to be disjoint and stably infinite. This paper surveys selected approaches to the problem of reasoning in the union of disjoint theories, that aim at going beyond equality sharing, including: asymmetric extensions of equality sharing, where some theories are unrestricted, while others must satisfy stronger requirements than stable infiniteness; superposition-based decision procedures; and current work on conflict-driven satisfiability (CDSAT).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    DPLL stands for Davis-Putnam-Logemann-Loveland and CDCL stands for Conflict-Driven Clause Learning. The CDCL procedure is an extension and improvement of the DPLL procedure.

  2. 2.

    Traditionally combination schemes use free variables for this role (e.g., [39]). Since quantified formulas appear in this paper, we choose to use free constants.

  3. 3.

    The spectrum of a theory is usually defined as the set of the finite cardinalities of its models. We extend the definition slightly for convenience.

References

  1. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_12

    Chapter  Google Scholar 

  2. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 65–80. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_4

    Chapter  MATH  Google Scholar 

  3. Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM TOCL 10(1), 129–179 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  4. Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  5. Baader, F., Ghilardi, S.: Connecting many-sorted structures and theories through adjoint functions. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 31–47. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_2

    Chapter  Google Scholar 

  6. Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229–255 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  7. Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symb. Comput. 21(2), 211–243 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  8. Baader, F., Schulz, K.U.: Combination of constraint solvers for free and quasi-free structures. Theor. Comput. Sci. 192(1), 107–161 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  9. Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Inf. Comput. 178(2), 346–390 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  10. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reasoning 31(2), 129–168 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  12. Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. Handbook of Model Checking, pp. 305–343. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_11

    Chapter  Google Scholar 

  13. Barrett, C.W., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  14. Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512–526. Springer, Heidelberg (2006). https://doi.org/10.1007/11916277_35

    Chapter  Google Scholar 

  15. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Maaren, H.V., Walsh, T. (eds.) Handbook of Satisfiability, Chap. 26, pp. 825–886. IOS Press (2009)

    Google Scholar 

  16. Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. J. Satisfiability Bool. Model. Comput. 3, 21–46 (2007)

    MATH  Google Scholar 

  17. Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116–130. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_11

    Chapter  Google Scholar 

  18. Bobot, F., Graham-Lengrand, S., Marre, B., Bury, G.: Centralizing equality reasoning in MCSAT. In: Proceedings of SMT-16 (2018)

    Google Scholar 

  19. Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M.J., Veloso, M. (eds.) Artificial Intelligence Today. LNCS (LNAI), vol. 1600, pp. 43–84. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48317-9_3

    Chapter  Google Scholar 

  20. Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fernàndez, M. (ed.) Proceedings of PPDP-12, pp. 1–11. ACM Press (2010)

    Google Scholar 

  21. Bonacina, M.P.: Parallel theorem proving. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 179–235. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63516-3_6

    Chapter  Google Scholar 

  22. Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM TOCL 8(1), 180–208 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  23. Bonacina, M.P., Echenim, M.: Generic theorem proving for decision procedures. TR 41/2006, Univ. degli Studi di Verona (2006). http://profs.sci.univr.it/~bonacina/rewsat.html. Revised March 2007

  24. Bonacina, M.P., Echenim, M.: \({\cal{T}}\)-decision by decomposition. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 199–214. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_14

    Chapter  Google Scholar 

  25. Bonacina, M.P., Echenim, M.: Rewrite-based decision procedures. In: Archer, M., Boy de la Tour, T., Muñoz, C. (eds.) Proceedings of STRATEGIES-6, volume 174(11) of ENTCS, pp. 27–45. Elsevier (2007)

    Google Scholar 

  26. Bonacina, M.P., Echenim, M.: Rewrite-based satisfiability procedures for recursive data structures. In: Cook, B., Sebastiani, R. (eds.) Proceedings of PDPAR-4, volume 174(8) of ENTCS, pp. 55–70. Elsevier (2007)

    Google Scholar 

  27. Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial \(\cal{T}\)-satisfiability procedures. J. Logic Comput. 18(1), 77–96 (2008)

    MathSciNet  MATH  Google Scholar 

  28. Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput. 45(2), 229–260 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  29. 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 (LNAI), vol. 4130, pp. 513–527. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_42

    Chapter  Google Scholar 

  30. Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. TR 308–06, Univ. degli Studi di Milano (2006). http://profs.sci.univr.it/~bonacina/rewsat.html

  31. Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Satisfiability modulo theories and assignments. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 42–59. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_4

    Chapter  Google Scholar 

  32. Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Proofs in conflict-driven theory combination. In: Andronick, J., Felty, A. (eds.) Proceedings of CPP-7, pp. 186–200. ACM Press (2018)

    Google Scholar 

  33. Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: transition system and completeness. J. Autom. Reasoning, 1–31 (2019, in press). https://doi.org/10.1007/s10817-018-09510-y

  34. Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theor. Comput. Sci. 146, 199–242 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  35. Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by DPLL(\(\Gamma +{\cal{T}}\)) and unsound theorem proving. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 35–50. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_3

    Chapter  Google Scholar 

  36. Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161–189 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  37. Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_12

    Chapter  Google Scholar 

  38. Bozzano, M., et al.: Efficient satisfiability modulo theories via delayed theory combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 335–349. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_34

    Chapter  Google Scholar 

  39. Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74113-8

    Book  MATH  Google Scholar 

  40. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_28

    Chapter  Google Scholar 

  41. Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_16

    Chapter  MATH  Google Scholar 

  42. Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_12

    Chapter  Google Scholar 

  43. Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 122–136. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_9

    Chapter  Google Scholar 

  44. Chocron, P., Fontaine, P., Ringeissen, C.: Politeness and combination methods for theories with bridging functions. J. Automat. Reasoning (2019). https://doi.org/10.1007/s10817-019-09512-4

  45. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7

    Chapter  MATH  Google Scholar 

  46. Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation. Logical Methods Comput. Sci. 8(3), 1–29 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  47. Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77–91. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9_8

    Chapter  Google Scholar 

  48. Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École Polytechnique, Univ. Paris-Saclay (2015)

    Google Scholar 

  49. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  50. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  51. de Moura, L., Bjørner, N.: Bugs, moles and skeletons: symbolic reasoning for software development. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 400–411. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_34

    Chapter  MATH  Google Scholar 

  52. de Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  53. de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1–12. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_1

    Chapter  Google Scholar 

  54. Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. Elsevier (1990)

    Google Scholar 

  55. Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, Chap. 9, pp. 535–610. Elsevier (2001)

    Google Scholar 

  56. Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  57. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Chapter  Google Scholar 

  58. Fermüller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, Chap. 25, pp. 1793–1849. Elsevier (2001)

    Google Scholar 

  59. Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409–425 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  60. Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 263–278. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_16

    Chapter  MATH  Google Scholar 

  61. Fontaine, P., Gribomont, E.P.: Combining non-stably infinite, non-first order theories. In: Ahrendt, W., Baumgartner, P., de Nivelle, H., Ranise, S., Tinelli, C. (eds.) Proceedings of PDPAR-2, volume 125 of ENTCS, pp. 37–51. Elsevier (2005)

    Google Scholar 

  62. Gallier, J.H., Snyder, W.: Designing unification procedures using transformations: a survey. Bull. EATCS 40, 273–326 (1990)

    MATH  Google Scholar 

  63. Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proceedings of LICS-14. IEEE Computer Society (1999)

    Google Scholar 

  64. Ganzinger, H., Rueß, H., Shankar, N.: Modularity and refinement in inference systems. Technical report, CSL-SRI-04-02, SRI International (2004)

    Google Scholar 

  65. Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 1–30. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_1

    Chapter  Google Scholar 

  66. Ghilardi, S., Nicolini, E., Zucchelli, D.: Recent advances in combined decision problems. In: Ballo, E., Franchella, M. (eds.) Logic and Philosophy in Italy: Trends and Perspectives, pp. 87–104. Polimetrica (2006)

    Google Scholar 

  67. Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM TOCL 9(2), 1–54 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  68. Graham-Lengrand, S., Jovanović, D.: An MCSAT treatment of bit-vectors. In: Brain, M., Hadarean, L. (eds.) Proceedings of SMT-15 (2017)

    Google Scholar 

  69. Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Cabodi, G., Singh, S. (eds.) Proceedings of FMCAD-12. ACM/IEEE (2012)

    Google Scholar 

  70. Hillenbrand, T.: Citius, altius, fortius: lessons learned from the theorem prover Waldmeister. In: Dahn, I., Vigneron, L. (eds.) Proceedings of FTP-4, volume 86 of ENTCS. Elsevier (2003)

    Google Scholar 

  71. Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 54–71. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-18088-5_6

    Chapter  Google Scholar 

  72. Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559–587 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  73. Huet, G.: A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Comput. Syst. Sci. 23(1), 11–21 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  74. Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  75. Jovanović, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330–346. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52234-0_18

    Chapter  Google Scholar 

  76. Jovanović, D., Barrett, C.W.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16242-8_29

    Chapter  Google Scholar 

  77. Jovanović, D., Barrett, C.W., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of FMCAD-13. ACM/IEEE (2013)

    Google Scholar 

  78. Jovanović, D., de Moura, L.: Cutting to the chase solving linear integer arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 338–353. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_26

    Chapter  Google Scholar 

  79. Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_27

    Chapter  Google Scholar 

  80. Jovanović, D., de Moura, L.: Cutting to the chase: solving linear integer arithmetic. J. Autom. Reasoning 51, 79–108 (2013)

    Article  MATH  Google Scholar 

  81. Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic combinability of rewriting-based satisfiability procedures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 542–556. Springer, Heidelberg (2006). https://doi.org/10.1007/11916277_37

    Chapter  Google Scholar 

  82. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Proceedings of Computational Problems in Abstract Algebras, pp. 263–298. Pergamon Press (1970)

    Google Scholar 

  83. Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509–523. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04244-7_41

    Chapter  Google Scholar 

  84. Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  85. Krstić, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS (LNAI), vol. 4720, pp. 1–27. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74621-8_1

    Chapter  Google Scholar 

  86. Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, Univ. of Texas at Austin (1975)

    Google Scholar 

  87. Lifschitz, V., Morgenstern, L., Plaisted, D.A.: Knowledge representation and classical logic. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 1, pp. 3–88. Elsevier (2008)

    Google Scholar 

  88. Lynch, C.A., Morawska, B.: Automatic decidability. In: Plotkin, G. (ed.) Proceedings of LICS-17. IEEE Computer Society (2002)

    Google Scholar 

  89. Lynch, C.A., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471–485. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45620-1_37

    Chapter  Google Scholar 

  90. Lynch, C.A., Ranise, S., Ringeissen, C., Tran, D.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026–1047 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  91. Lynch, C.A., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 328–344. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_22

    Chapter  Google Scholar 

  92. Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 381–422. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40007-3_24

    Chapter  Google Scholar 

  93. Marques Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  94. Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 131–153. IOS Press (2009)

    Google Scholar 

  95. McCarthy, J.W.: Towards a mathematical science of computation. In: Popplewell, C.M. (ed.) Proceedings of IFIP 1962, North Holland, pp. 21–28 (1963)

    Google Scholar 

  96. McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_35

    Chapter  Google Scholar 

  97. Nelson, G.: Techniques for program verification. Technical report, CSL-81-10, Xerox, Palo Alto Research Center (1981)

    Google Scholar 

  98. Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201–211. American Mathematical Society (1983)

    Google Scholar 

  99. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  100. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  101. Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 319–334. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_20

    Chapter  MATH  Google Scholar 

  102. Nieuwenhuis, R.: Decidability and complexity analysis by basic paramodulation. Inf. Comput. 147(1), 1–21 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  103. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  104. Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, Chap. 7, pp. 371–443. Elsevier (2001)

    Google Scholar 

  105. Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291–302 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  106. Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, volume I: Logical Foundations, pp. 273–364. Oxford University Press (1993)

    Google Scholar 

  107. Plaisted, D.A.: Automated theorem proving. Wiley Interdisc. Rev. Cogn. Sci. 5(2), 115–128 (2014)

    Article  MathSciNet  Google Scholar 

  108. Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005). https://doi.org/10.1007/11559306_3

    Chapter  MATH  Google Scholar 

  109. Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 399–415. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_28

    Chapter  Google Scholar 

  110. Ringeissen, C.: Cooperation of decision procedures for the satisfiability problem. In: Baader, F., Schulz, K.U. (eds.) Proceedings of FroCoS-1, Applied Logic, Kluwer, pp. 121–140 (1996)

    Google Scholar 

  111. Ringeissen, C., Senni, V.: Modular termination and combinability for superposition modulo counter arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 211–226. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_15

    Chapter  Google Scholar 

  112. Robinson, G.A., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Michie, D., Meltzer, B. (eds.) Machine Intelligence, vol. 4, pp. 135–150. Edinburgh University Press (1969)

    Google Scholar 

  113. Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symb. Comput. 11(1 & 2), 21–50 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  114. Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_49

    Chapter  Google Scholar 

  115. Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisfiability Bool. Model. and Comput. 3, 141–224 (2007)

    MathSciNet  MATH  Google Scholar 

  116. Shankar, N.: Automated deduction for verification. ACM Comput. Surv. 41(4), 40–96 (2009)

    Article  Google Scholar 

  117. Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583–585 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  118. Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 67–83. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_5

    Chapter  Google Scholar 

  119. Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Proceedings of FroCoS-1, Applied Logic, pp. 103–120. Kluwer (1996)

    Google Scholar 

  120. Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291–353 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  121. Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 641–653. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30227-8_53

    Chapter  Google Scholar 

  122. Tinelli, C., Zarba, C.G.: Combining non-stably infinite theories. J. Autom. Reasoning 34(3), 209–238 (2005)

    Article  MATH  Google Scholar 

  123. Wang, C., Ivančić, F., Ganai, M., Gupta, A.: Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 322–336. Springer, Heidelberg (2005). https://doi.org/10.1007/11591191_23

    Chapter  MATH  Google Scholar 

  124. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140–145. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_10

    Chapter  Google Scholar 

  125. Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 366–382. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_23

    Chapter  MATH  Google Scholar 

  126. Wolfman, S.A., Weld, D.S.: The LPSAT engine and its application to resource planning. In: Dean, T. (ed.) Proceedings of IJCAI-16, vol. 1, pp. 310–316. Morgan Kaufmann (1999)

    Google Scholar 

  127. Zeljić, A., Wintersteiger, C.M., Rümmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249–266. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_16

    Chapter  Google Scholar 

Download references

Acknowledgments

The authors thank the co-authors of their papers covered in this survey. Part of this work was done when the first author was visiting LORIA Nancy and the Computer Science Laboratory of SRI International: the support of both institutions is greatly appreciated. This work was funded in part by grant “Ricerca di base 2017” of the Università degli Studi di Verona.

Author information

Authors and Affiliations

  1. Università degli Studi di Verona, Verona, Italy

    Maria Paola Bonacina

  2. Université de Lorraine and Inria & LORIA, Nancy, France

    Pascal Fontaine & Christophe Ringeissen

  3. The University of Iowa, Iowa City, USA

    Cesare Tinelli

Authors
  1. Maria Paola Bonacina
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pascal Fontaine
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christophe Ringeissen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Cesare Tinelli
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maria Paola Bonacina .

Editor information

Editors and Affiliations

  1. University of Bremen, Bremen, Germany

    Carsten Lutz

  2. University of Manchester, Manchester, UK

    Uli Sattler

  3. University of Iowa, Iowa City, IA, USA

    Cesare Tinelli

  4. TU Dresden, Dresden, Germany

    Anni-Yasmin Turhan

  5. University of Liverpool, Liverpool, UK

    Frank Wolter

Additional information

Dedicated to Franz Baader friend and colleague.

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C. (2019). Theory Combination: Beyond Equality Sharing. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, AY., Wolter, F. (eds) Description Logic, Theory Combination, and All That. Lecture Notes in Computer Science(), vol 11560. Springer, Cham. https://doi.org/10.1007/978-3-030-22102-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-22102-7_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-22101-0

  • Online ISBN: 978-3-030-22102-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation