{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:17Z","timestamp":1767928337907,"version":"3.49.0"},"publisher-location":"Cham","reference-count":127,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030221010","type":"print"},{"value":"9783030221027","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22102-7_3","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T12:21:26Z","timestamp":1561465286000},"page":"57-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Theory Combination: Beyond Equality Sharing"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, 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\u2013150. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11559306_4","volume-title":"Frontiers of Combining Systems","author":"A Armando","year":"2005","unstructured":"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\u201380. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_4"},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM TOCL 10(1), 129\u2013179 (2009)","journal-title":"ACM TOCL"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11559306_2","volume-title":"Frontiers of Combining Systems","author":"F Baader","year":"2005","unstructured":"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\u201347. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_2"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0304-3975(94)00277-0","volume":"142","author":"F Baader","year":"1995","unstructured":"Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theor. Comput. Sci. 142(2), 229\u2013255 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"3_CR7","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symb. Comput. 21(2), 211\u2013243 (1996)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"3_CR8","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0304-3975(97)00147-3","volume":"192","author":"F Baader","year":"1998","unstructured":"Baader, F., Schulz, K.U.: Combination of constraint solvers for free and quasi-free structures. Theor. Comput. Sci. 192(1), 107\u2013161 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1006\/inco.2001.3118","volume":"178","author":"F Baader","year":"2002","unstructured":"Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Inf. Comput. 178(2), 346\u2013390 (2002)","journal-title":"Inf. Comput."},{"issue":"3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Logic Comput."},{"issue":"2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reasoning 31(2), 129\u2013168 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"CW Barrett","year":"2018","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"CW Barrett","year":"2011","unstructured":"Barrett, C.W., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"CW Barrett","year":"2006","unstructured":"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\u2013526. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_35"},{"key":"3_CR15","unstructured":"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\u2013886. IOS Press (2009)"},{"key":"3_CR16","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"CW Barrett","year":"2007","unstructured":"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\u201346 (2007)","journal-title":"J. Satisfiability Bool. Model. Comput."},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116\u2013130. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11"},{"key":"3_CR18","unstructured":"Bobot, F., Graham-Lengrand, S., Marre, B., Bury, G.: Centralizing equality reasoning in MCSAT. In: Proceedings of SMT-16 (2018)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/3-540-48317-9_3","volume-title":"Artificial Intelligence Today","author":"MP Bonacina","year":"1999","unstructured":"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\u201384. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48317-9_3"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fern\u00e0ndez, M. (ed.) Proceedings of PPDP-12, pp. 1\u201311. ACM Press (2010)","DOI":"10.1145\/1836089.1836090"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-63516-3_6","volume-title":"Handbook of Parallel Constraint Reasoning","author":"MP Bonacina","year":"2018","unstructured":"Bonacina, M.P.: Parallel theorem proving. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 179\u2013235. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_6"},{"issue":"1","key":"3_CR22","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"MP Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM TOCL 8(1), 180\u2013208 (2007)","journal-title":"ACM TOCL"},{"key":"3_CR23","unstructured":"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"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-73595-3_14","volume-title":"Automated Deduction \u2013 CADE-21","author":"MP Bonacina","year":"2007","unstructured":"Bonacina, M.P., Echenim, M.: $${\\cal{T}}$$ -decision by decomposition. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 199\u2013214. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_14"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Echenim, M.: Rewrite-based decision procedures. In: Archer, M., Boy de la Tour, T., Mu\u00f1oz, C. (eds.) Proceedings of STRATEGIES-6, volume 174(11) of ENTCS, pp. 27\u201345. Elsevier (2007)","DOI":"10.1016\/j.entcs.2006.11.042"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"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\u201370. Elsevier (2007)","DOI":"10.1016\/j.entcs.2006.11.039"},{"issue":"1","key":"3_CR27","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1093\/logcom\/exm055","volume":"18","author":"MP Bonacina","year":"2008","unstructured":"Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial $$\\cal{T}$$ -satisfiability procedures. J. Logic Comput. 18(1), 77\u201396 (2008)","journal-title":"J. Logic Comput."},{"issue":"2","key":"3_CR28","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.jsc.2008.10.008","volume":"45","author":"MP Bonacina","year":"2010","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput. 45(2), 229\u2013260 (2010)","journal-title":"J. Symb. Comput."},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/11814771_42","volume-title":"Automated Reasoning","author":"MP Bonacina","year":"2006","unstructured":"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\u2013527. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_42"},{"key":"3_CR30","unstructured":"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\u201306, Univ. degli Studi di Milano (2006). http:\/\/profs.sci.univr.it\/~bonacina\/rewsat.html"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-63046-5_4","volume-title":"Automated Deduction \u2013 CADE 26","author":"MP Bonacina","year":"2017","unstructured":"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\u201359. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_4"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"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\u2013200. ACM Press (2018)","DOI":"10.1145\/3167096"},{"key":"3_CR33","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: transition system and completeness. J. Autom. Reasoning, 1\u201331 (2019, in press). https:\/\/doi.org\/10.1007\/s10817-018-09510-y","DOI":"10.1007\/s10817-018-09510-y"},{"key":"3_CR34","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"MP Bonacina","year":"1995","unstructured":"Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theor. Comput. Sci. 146, 199\u2013242 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-02959-2_3","volume-title":"Automated Deduction \u2013 CADE-22","author":"MP Bonacina","year":"2009","unstructured":"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\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_3"},{"issue":"2","key":"3_CR36","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/11513988_34","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2005","unstructured":"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\u2013349. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_34"},{"key":"3_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation - Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"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"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"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\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"3_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150\u2013153. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12"},{"key":"3_CR43","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-08587-6_9","volume-title":"Automated Reasoning","author":"P Chocron","year":"2014","unstructured":"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\u2013136. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_9"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1007\/s10817-019-09512-4"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"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\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"issue":"3","key":"3_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(3:16)2012","volume":"8","author":"S Conchon","year":"2012","unstructured":"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\u201329 (2012)","journal-title":"Logical Methods Comput. Sci."},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15297-9_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Cotton","year":"2010","unstructured":"Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77\u201391. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_8"},{"key":"3_CR48","unstructured":"Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, \u00c9cole Polytechnique, Univ. Paris-Saclay (2015)"},{"issue":"7","key":"3_CR49","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"3_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR51","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-642-14203-1_34","volume-title":"Automated Reasoning","author":"L Moura de","year":"2010","unstructured":"de Moura, L., Bj\u00f8rner, N.: Bugs, moles and skeletons: symbolic reasoning for software development. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 400\u2013411. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_34"},{"issue":"9","key":"3_CR52","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura de","year":"2011","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"3_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"key":"3_CR54","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"3_CR55","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, Chap. 9, pp. 535\u2013610. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"issue":"3","key":"3_CR56","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"DL Detlefs","year":"2005","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"3_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"3_CR58","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, 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\u20131849. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50027-8"},{"issue":"4","key":"3_CR59","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s11786-012-0134-5","volume":"6","author":"A Fietzke","year":"2012","unstructured":"Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409\u2013425 (2012)","journal-title":"Math. Comput. Sci."},{"key":"3_CR60","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-04222-5_16","volume-title":"Frontiers of Combining Systems","author":"P Fontaine","year":"2009","unstructured":"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\u2013278. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_16"},{"key":"3_CR61","doi-asserted-by":"crossref","unstructured":"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\u201351. Elsevier (2005)","DOI":"10.1016\/j.entcs.2004.06.066"},{"key":"3_CR62","first-page":"273","volume":"40","author":"JH Gallier","year":"1990","unstructured":"Gallier, J.H., Snyder, W.: Designing unification procedures using transformations: a survey. Bull. EATCS 40, 273\u2013326 (1990)","journal-title":"Bull. EATCS"},{"key":"3_CR63","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proceedings of LICS-14. IEEE Computer Society (1999)"},{"key":"3_CR64","unstructured":"Ganzinger, H., Rue\u00df, H., Shankar, N.: Modularity and refinement in inference systems. Technical report, CSL-SRI-04-02, SRI International (2004)"},{"key":"3_CR65","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11559306_1","volume-title":"Frontiers of Combining Systems","author":"S Ghilardi","year":"2005","unstructured":"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\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_1"},{"key":"3_CR66","unstructured":"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\u2013104. Polimetrica (2006)"},{"issue":"2","key":"3_CR67","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1342991.1342992","volume":"9","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM TOCL 9(2), 1\u201354 (2008)","journal-title":"ACM TOCL"},{"key":"3_CR68","unstructured":"Graham-Lengrand, S., Jovanovi\u0107, D.: An MCSAT treatment of bit-vectors. In: Brain, M., Hadarean, L. (eds.) Proceedings of SMT-15 (2017)"},{"key":"3_CR69","unstructured":"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)"},{"key":"3_CR70","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1016\/S1571-0661(04)80649-2"},{"key":"3_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Automata, Languages and Programming","author":"J Hsiang","year":"1987","unstructured":"Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 54\u201371. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18088-5_6"},{"issue":"3","key":"3_CR72","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559\u2013587 (1991)","journal-title":"J. ACM"},{"issue":"1","key":"3_CR73","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G Huet","year":"1981","unstructured":"Huet, G.: A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Comput. Syst. Sci. 23(1), 11\u201321 (1981)","journal-title":"J. Comput. Syst. Sci."},{"issue":"4","key":"3_CR74","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J-P Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"3_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-52234-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Jovanovi\u0107","year":"2017","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330\u2013346. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_18"},{"key":"3_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.W.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402\u2013416. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_29"},{"key":"3_CR77","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, 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)","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"3_CR78","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-22438-6_26","volume-title":"Automated Deduction \u2013 CADE-23","author":"D Jovanovi\u0107","year":"2011","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the chase solving linear integer arithmetic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 338\u2013353. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_26"},{"key":"3_CR79","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"3_CR80","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the chase: solving linear integer arithmetic. J. Autom. Reasoning 51, 79\u2013108 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR81","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/11916277_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H Kirchner","year":"2006","unstructured":"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\u2013556. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_37"},{"key":"3_CR82","doi-asserted-by":"crossref","unstructured":"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\u2013298. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"3_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-04244-7_41","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K Korovin","year":"2009","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509\u2013523. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04244-7_41"},{"key":"3_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"3_CR85","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, 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\u201327. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74621-8_1"},{"key":"3_CR86","unstructured":"Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, Univ. of Texas at Austin (1975)"},{"key":"3_CR87","doi-asserted-by":"crossref","unstructured":"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\u201388. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03001-5"},{"key":"3_CR88","unstructured":"Lynch, C.A., Morawska, B.: Automatic decidability. In: Plotkin, G. (ed.) Proceedings of LICS-17. IEEE Computer Society (2002)"},{"key":"3_CR89","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45620-1_37","volume-title":"Automated Deduction\u2014CADE-18","author":"CA Lynch","year":"2002","unstructured":"Lynch, C.A., Morawska, B.: Basic syntactic mutation. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 471\u2013485. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_37"},{"issue":"7","key":"3_CR90","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1016\/j.ic.2011.03.005","volume":"209","author":"CA Lynch","year":"2011","unstructured":"Lynch, C.A., Ranise, S., Ringeissen, C., Tran, D.: Automatic decidability and combinability. Inf. Comput. 209(7), 1026\u20131047 (2011)","journal-title":"Inf. Comput."},{"key":"3_CR91","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-73595-3_22","volume-title":"Automated Deduction \u2013 CADE-21","author":"CA Lynch","year":"2007","unstructured":"Lynch, C.A., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 328\u2013344. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_22"},{"key":"3_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-40007-3_24","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"Z Manna","year":"2003","unstructured":"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\u2013422. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-40007-3_24"},{"issue":"5","key":"3_CR93","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J Marques Silva","year":"1999","unstructured":"Marques Silva, J., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR94","unstructured":"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\u2013153. IOS Press (2009)"},{"key":"3_CR95","unstructured":"McCarthy, J.W.: Towards a mathematical science of computation. In: Popplewell, C.M. (ed.) Proceedings of IFIP 1962, North Holland, pp. 21\u201328 (1963)"},{"key":"3_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2009","unstructured":"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\u2013476. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_35"},{"key":"3_CR97","unstructured":"Nelson, G.: Techniques for program verification. Technical report, CSL-81-10, Xerox, Palo Alto Research Center (1981)"},{"key":"3_CR98","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201\u2013211. American Mathematical Society (1983)","DOI":"10.1090\/conm\/029\/11"},{"issue":"2","key":"3_CR99","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"issue":"2","key":"3_CR100","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"3_CR101","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-04222-5_20","volume-title":"Frontiers of Combining Systems","author":"E Nicolini","year":"2009","unstructured":"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\u2013334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_20"},{"issue":"1","key":"3_CR102","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2730","volume":"147","author":"R Nieuwenhuis","year":"1998","unstructured":"Nieuwenhuis, R.: Decidability and complexity analysis by basic paramodulation. Inf. Comput. 147(1), 1\u201321 (1998)","journal-title":"Inf. Comput."},{"issue":"6","key":"3_CR103","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"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\u2013977 (2006)","journal-title":"J. ACM"},{"key":"3_CR104","doi-asserted-by":"crossref","unstructured":"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\u2013443. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"3_CR105","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR106","doi-asserted-by":"crossref","unstructured":"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\u2013364. Oxford University Press (1993)","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"issue":"2","key":"3_CR107","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1002\/wcs.1269","volume":"5","author":"DA Plaisted","year":"2014","unstructured":"Plaisted, D.A.: Automated theorem proving. Wiley Interdisc. Rev. Cogn. Sci. 5(2), 115\u2013128 (2014)","journal-title":"Wiley Interdisc. Rev. Cogn. Sci."},{"key":"3_CR108","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S Ranise","year":"2005","unstructured":"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\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_3"},{"key":"3_CR109","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-319-21401-6_28","volume-title":"Automated Deduction - CADE-25","author":"G Reger","year":"2015","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 399\u2013415. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_28"},{"key":"3_CR110","doi-asserted-by":"crossref","unstructured":"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\u2013140 (1996)","DOI":"10.1007\/978-94-009-0349-4_6"},{"key":"3_CR111","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-642-24364-6_15","volume-title":"Frontiers of Combining Systems","author":"C Ringeissen","year":"2011","unstructured":"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\u2013226. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24364-6_15"},{"key":"3_CR112","unstructured":"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\u2013150. Edinburgh University Press (1969)"},{"issue":"1 & 2","key":"3_CR113","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M Rusinowitch","year":"1991","unstructured":"Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symb. Comput. 11(1 & 2), 21\u201350 (1991)","journal-title":"J. Symb. Comput."},{"key":"3_CR114","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"key":"3_CR115","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisfiability Bool. Model. and Comput. 3, 141\u2013224 (2007)","journal-title":"J. Satisfiability Bool. Model. and Comput."},{"issue":"4","key":"3_CR116","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1592434.1592437","volume":"41","author":"N Shankar","year":"2009","unstructured":"Shankar, N.: Automated deduction for verification. ACM Comput. Surv. 41(4), 40\u201396 (2009)","journal-title":"ACM Comput. Surv."},{"issue":"7","key":"3_CR117","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"RE Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583\u2013585 (1978)","journal-title":"Commun. ACM"},{"key":"3_CR118","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-02959-2_5","volume-title":"Automated Deduction \u2013 CADE-22","author":"V Sofronie-Stokkermans","year":"2009","unstructured":"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\u201383. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_5"},{"key":"3_CR119","doi-asserted-by":"crossref","unstructured":"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\u2013120. Kluwer (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"1","key":"3_CR120","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291\u2013353 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR121","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logics in Artificial Intelligence","author":"C Tinelli","year":"2004","unstructured":"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\u2013653. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30227-8_53"},{"issue":"3","key":"3_CR122","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining non-stably infinite theories. J. Autom. Reasoning 34(3), 209\u2013238 (2005)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR123","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/11591191_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Wang","year":"2005","unstructured":"Wang, C., Ivan\u010di\u0107, 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\u2013336. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_23"},{"key":"3_CR124","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"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\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"},{"key":"3_CR125","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-04222-5_23","volume-title":"Frontiers of Combining Systems","author":"T Wies","year":"2009","unstructured":"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\u2013382. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_23"},{"key":"3_CR126","unstructured":"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\u2013316. Morgan Kaufmann (1999)"},{"key":"3_CR127","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-40970-2_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"A Zelji\u0107","year":"2016","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249\u2013266. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_16"}],"container-title":["Lecture Notes in Computer Science","Description Logic, Theory Combination, and All That"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22102-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,20]],"date-time":"2024-07-20T05:33:58Z","timestamp":1721453638000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22102-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030221010","9783030221027"],"references-count":127,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22102-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}