M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A modular integration of SAT/SMT solvers to Coq through proof witnesses, Proc. of CPP-1, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal, Proc. of FroCoS-5, vol.3717, pp.65-80, 2005.

A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz, New results on rewritebased satisfiability procedures, vol.10, pp.129-179, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00576862

A. Armando, S. Ranise, and M. Rusinowitch, A rewriting approach to satisfiability procedures, Inform. Comput, vol.183, issue.2, pp.140-164, 2003.

F. Baader and S. Ghilardi, Connecting many-sorted structures and theories through adjoint functions, Proc. of FroCoS-5, vol.3717, pp.31-47, 2005.

F. Baader and K. U. Schulz, Combination techniques and decision problems for disunification, Theor. Comput. Sci, vol.142, issue.2, pp.229-255, 1995.

F. Baader and K. U. Schulz, Unification in the union of disjoint equational theories: Combining decision procedures, J. Symb. Comput, vol.21, issue.2, pp.211-243, 1996.

F. Baader and K. U. Schulz, Combination of constraint solvers for free and quasifree structures, Theor. Comput. Sci, vol.192, issue.1, pp.107-161, 1998.

F. Baader and C. Tinelli, Deciding the word problem in the union of equational theories, Inform. Comput, vol.178, issue.2, pp.346-390, 2002.

L. Bachmair and H. Ganzinger, Rewrite-based equational theorem proving with selection and simplification, J. Logic and Comput, vol.4, issue.3, pp.217-247, 1994.

L. Bachmair, A. Tiwari, and L. Vigneron, Abstract congruence closure. J. Automat. Reason, vol.31, issue.2, pp.129-168, 2003.

C. W. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi? et al., Proc. of CAV-23, vol.6806, pp.171-177, 2011.

C. W. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Splitting on demand in SAT modulo theories, Proc. of LPAR-13, vol.4246, pp.512-526, 2006.

C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories, Handbook of Satisfiability, vol.26, pp.825-886, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

C. W. Barrett, I. Shikanian, and C. Tinelli, An abstract decision procedure for satisfiability in the theory of inductive data types, J. Satisfiability Bool. Model. and Comput, vol.3, pp.21-46, 2007.

C. W. Barrett and C. Tinelli, Satisfiability modulo theories, Handbook of Model Checking, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01095009

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT solvers, Proc. of CADE-23, vol.6803, pp.116-130, 2011.

F. Bobot, S. Graham-lengrand, B. Marre, and G. Bury, Centralizing equality reasoning in MCSAT, Proc of SMT-16, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01935591

M. P. Bonacina, A taxonomy of theorem-proving strategies, Artificial Intelligence Today -Recent Trends and Developments, volume 1600 of LNAI, pp.43-84, 1999.

M. P. Bonacina, On theorem proving for program checking -Historical perspective and recent developments, Proc. of PPDP-12, pp.1-11, 2010.

M. P. Bonacina, Parallel theorem proving, Handbook of Parallel Constraint Reasoning, pp.179-235, 2018.

M. P. Bonacina and N. Dershowitz, Abstract canonical inference. ACM TOCL, vol.8, issue.1, pp.180-208, 2007.

M. P. Bonacina and M. Echenim, Generic theorem proving for decision procedures. TR 41, 2006.

M. P. Bonacina and M. Echenim, T -decision by decomposition, Proc. of CADE-21, vol.4603, pp.199-214, 2007.

M. P. Bonacina and M. Echenim, Rewrite-based decision procedures, Proc. of STRATEGIES-6, vol.174, pp.27-45, 2007.

M. P. Bonacina and M. Echenim, Rewrite-based satisfiability procedures for recursive data structures, Proc. of PDPAR-4, vol.174, pp.55-70, 2007.

M. P. Bonacina and M. Echenim, On variable-inactivity and polynomial Tsatisfiability procedures, J. Logic and Comput, vol.18, issue.1, pp.77-96, 2008.

M. P. Bonacina and M. Echenim, Theory decision by decomposition, J. Symb. Comput, vol.45, issue.2, pp.229-260, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00940845

M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures, Proc. of IJCAR-3, vol.4130, pp.513-527, 2006.

M. P. Bonacina, S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli, Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. TR 308-06, Univ. degli Studi di Milano, 2006.

M. P. Bonacina, S. Graham-lengrand, and N. Shankar, Satisfiability modulo theories and assignments, Proc. of CADE-26, vol.10395, pp.42-59, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01615830

M. P. Bonacina, S. Graham-lengrand, and N. Shankar, Proofs in conflict-driven theory combination, Proc. of CPP-7, pp.186-200, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01935595

M. P. Bonacina, S. Graham-lengrand, and N. Shankar, Conflict-driven satisfiability for theory combination: Transition system and completeness, J. Automat. Reason, 2019.

M. P. Bonacina and J. Hsiang, Towards a foundation of completion procedures as semidecision procedures, Theor. Comput. Sci, vol.146, pp.199-242, 1995.

M. P. Bonacina, C. A. Lynch, and L. De-moura, On deciding satisfiability by DPLL(? + T ) and unsound theorem proving, Proc. of CADE-22, vol.5663, pp.35-50, 2009.

M. P. Bonacina, C. A. Lynch, and L. De-moura, On deciding satisfiability by theorem proving with speculative inferences, J. Automat. Reason, vol.47, issue.2, pp.161-189, 2011.

T. Bouton, D. Caminha, B. De-oliveira, D. Déharbe, and P. Fontaine, veriT: an open, trustable and efficient SMT-solver, Proc. of CADE-22, vol.5663, pp.151-156, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430634

M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, S. Ranise et al., Efficient satisfiability modulo theories via delayed theory combination, Proc. of CAV-17, vol.3576, pp.335-349, 2005.

A. R. Bradley and Z. Manna, The Calculus of Computation -Decision Procedures with Applications to Verification, 2007.

A. R. Bradley, Z. Manna, and H. B. Sipma, What's decidable about arrays, Proc. of VMCAI-7, vol.3055, pp.427-442, 2006.

R. Brummayer and A. Biere, Boolector: An efficient SMT solver for bit-vectors and arrays, Proc. of TACAS-15, vol.5505, pp.174-177, 2009.

R. Bruttomesso, E. Pek, N. Sharygina, and A. Tsitovich, The OpenSMT solver, Proc. of TACAS-16, vol.6015, pp.150-153, 2010.

P. Chocron, P. Fontaine, and C. Ringeissen, A gentle non-disjoint combination of satisfiability procedures, Proc. of IJCAR-7, vol.8562, pp.122-136, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01087162

P. Chocron, P. Fontaine, and C. Ringeissen, Politeness and combination methods for theories with bridging functions, J. Automat. Reason, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01988452

A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani, The MathSAT5 SMT solver, Proc. of TACAS-19, vol.7795, pp.93-107, 2013.

S. Conchon, E. Contejean, and M. Iguernelala, Canonized rewriting and ground AC completion modulo Shostak theories : Design and implementation, Logical Methods in Computer Science, vol.8, issue.3, pp.1-29, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00798082

S. Cotton, Natural domain SMT: A preliminary assessment, Proc. of FORMATS-8, vol.6246, pp.77-91, 2010.

S. Cruanes, Extending superposition with integer arithmetic, structural induction, and beyond, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01223502

M. Davis, G. Logemann, and D. Loveland, A machine program for theoremproving, Commun. ACM, vol.5, issue.7, pp.394-397, 1962.

L. De-moura and N. Bjørner, Z3: an efficient SMT solver, Proc. of TACAS-14, vol.4963, pp.337-340

. Springer, , 2008.

L. De-moura and N. Bjørner, Bugs, moles and skeletons: symbolic reasoning for software development, Proc. of IJCAR-5, vol.6173, pp.400-411, 2010.

L. De-moura and N. Bjørner, Satisfiability modulo theories: introduction and applications, Commun. ACM, vol.54, issue.9, pp.69-77, 2011.

L. De-moura and D. Jovanovi?, A model-constructing satisfiability calculus, Proc. of VMCAI-14, vol.7737, pp.1-12, 2013.

N. Dershowitz and J. Jouannaud, Rewrite systems, Handbook of Theoretical Computer Science, vol.B, pp.243-320, 1990.

N. Dershowitz and D. A. , Plaisted. Rewriting, Handbook of Automated Reasoning, vol.1, pp.535-610, 2001.

D. L. Detlefs, G. Nelson, and J. B. Saxe, Simplify: a theorem prover for program checking, J. ACM, vol.52, issue.3, pp.365-473, 2005.

B. Dutertre, Yices 2.2, Proc. of CAV-26, vol.8559, pp.737-744, 2014.

C. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet, Resolution decision procedures, Handbook of Automated Reasoning, vol.II, pp.1793-1849, 2001.

A. Fietzke and C. Weidenbach, Superposition as a decision procedure for timed automata, Mathematics in Computer Science, vol.6, issue.4, pp.409-425, 2012.

P. Fontaine, Combinations of theories for decidable fragments of first-order logic, Proc. of FroCoS-7, vol.5749, pp.263-278, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430631

P. Fontaine and E. P. Gribomont, Combining non-stably infinite, non-first order theories, Proc. of PDPAR-2, vol.125, pp.37-51, 2005.

J. H. Gallier and W. Snyder, Designing unification procedures using transformations: a survey, Bulletin of the EATCS, vol.40, pp.273-326, 1990.

H. Ganzinger and H. De-nivelle, A superposition decision procedure for the guarded fragment with equality, Proc. of LICS-14, 1999.

H. Ganzinger, H. Rueß, and N. Shankar, Modularity and refinement in inference systems, 2004.

S. Ghilardi, E. Nicolini, and D. Zucchelli, A comprehensive framework for combining decision procedures, Proc. of FroCoS-5, vol.3717, pp.1-30, 2005.

S. Ghilardi, E. Nicolini, and D. Zucchelli, Recent advances in combined decision problems, Logic and Philosophy in Italy: Trends and Perspectives, pp.87-104, 2006.

S. Ghilardi, E. Nicolini, and D. Zucchelli, A comprehensive combination framework, vol.9, pp.1-54, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00576602

S. Graham-lengrand and D. Jovanovi?, An MCSAT treatment of bit-vectors, Proc. of SMT-15, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01615837

L. Haller, A. Griggio, M. Brain, and D. Kroening, Deciding floating-point logic with systematic abstraction, Proc. of FMCAD-12, 2012.

T. Hillenbrand, Citius, altius, fortius: lessons learned from the theorem prover Waldmeister, Proc. of FTP-4, vol.86, 2003.

J. Hsiang and M. Rusinowitch, On word problems in equational theories, Proc. of ICALP-14, vol.267, pp.54-71
URL : https://hal.archives-ouvertes.fr/inria-00075875

. Springer, , 1987.

J. Hsiang and M. Rusinowitch, Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method, J. ACM, vol.38, issue.3, pp.559-587, 1991.

G. Huet, A complete proof of correctness of the Knuth-Bendix completion algorithm, J. Comput. Syst. Sci, vol.23, issue.1, pp.11-21, 1981.
URL : https://hal.archives-ouvertes.fr/inria-00076536

J. Jouannaud and H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput, vol.15, issue.4, pp.1155-1194, 1986.

D. Jovanovi?, Solving nonlinear integer arithmetic with MCSAT, Proc. of VMCAI-18, vol.10145, pp.330-346, 2017.

D. Jovanovi? and C. W. Barrett, Polite theories revisited, Proc. of LPAR-17, vol.6397, pp.402-443

. Springer, , 2010.

D. Jovanovi?, C. W. Barrett, and L. De-moura, The design and implementation of the model-constructing satisfiability calculus, Proc. of FMCAD-13, 2013.

D. Jovanovi? and L. De-moura, Cutting to the chase: solving linear integer arithmetic, Proc. of CADE-23, vol.6803, pp.338-353, 2011.

D. Jovanovi? and L. De-moura, Solving non-linear arithmetic, Proc. of IJCAR-6, vol.7364, pp.339-354, 2012.

D. Jovanovi? and L. De-moura, Cutting to the chase: solving linear integer arithmetic, J. Automat. Reason, vol.51, pp.79-108, 2013.

H. Kirchner, S. Ranise, C. Ringeissen, and D. Tran, Automatic combinability of rewriting-based satisfiability procedures, Proc. of LPAR-13, vol.4246, pp.542-556, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00117261

D. E. Knuth and P. B. Bendix, Simple word problems in universal algebras, Proc. of Computational Problems in Abstract Algebras, pp.263-298, 1970.

K. Korovin, N. Tsiskaridze, and A. Voronkov, Conflict resolution, Proc. of CP-15, vol.5732, 2009.

L. Kovàcs and A. Voronkov, First order theorem proving and Vampire, Proc. of CAV-25, vol.8044, pp.1-35, 2013.

S. Krsti? and A. Goel, Architecting solvers for SAT modulo theories: NelsonOppen with DPLL, Proc. of FroCoS-6, vol.4720, pp.1-27, 2007.

D. S. Lankford, Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, 1975.

V. Lifschitz, L. Morgenstern, and D. A. Plaisted, Knowledge representation and classical logic, Handbook of Knowledge Representation, vol.1, pp.3-88, 2008.

C. A. Lynch and B. Morawska, Automatic decidability, Proc. of LICS-17, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00586936

C. A. Lynch and B. Morawska, Basic syntactic mutation, Proc. of CADE-18, volume 2392 of LNAI, pp.471-485, 2002.

C. A. Lynch, S. Ranise, C. Ringeissen, and D. Tran, Automatic decidability and combinability, Inf. Comput, vol.209, issue.7, pp.1026-1047, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00586936

C. A. Lynch and D. Tran, Automatic decidability and combinability revisited, Proc. of CADE-21, vol.4603, pp.328-344
URL : https://hal.archives-ouvertes.fr/inria-00576605

. Springer, , 2007.

Z. Manna and C. G. Zarba, Combining decision procedures, Formal Methods at the Crossroads. From Panacea to Foundational Support, vol.2757, pp.381-422, 2002.

J. Silva and K. A. Sakallah, GRASP: A search algorithm for propositional satisfiability, IEEE Trans. on Computers, vol.48, issue.5, pp.506-521, 1999.

J. P. Silva, I. Lynce, and S. Malik, Conflict-driven clause learning SAT solvers, Handbook of Satisfiability, vol.185, pp.131-153, 2009.

J. W. Mccarthy, Towards a mathematical science of computation, Proc. of IFIP 1962, pp.21-28, 1963.

K. L. Mcmillan, A. Kuehlmann, and M. Sagiv, Generalizing DPLL to richer logics, Proc. of CAV-21, vol.5643, pp.462-476, 2009.

G. Nelson, Techniques for program verification, 1981.

G. Nelson, Combining satisfiability procedures by equality sharing, Automatic Theorem Proving: After 25 Years, pp.201-211, 1983.

G. Nelson and D. C. Oppen, Simplification by cooperating decision procedures, ACM TOPLAS, vol.1, issue.2, pp.245-257, 1979.

G. Nelson and D. C. Oppen, Fast decision procedures based on congruence closure, J. ACM, vol.27, issue.2, pp.356-364, 1980.

E. Nicolini, C. Ringeissen, and M. Rusinowitch, Data structures with arithmetic constraints: a non-disjoint combination, Proc. of FroCoS-7, vol.5749, pp.319-334, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00397080

R. Nieuwenhuis, Decidability and complexity analysis by basic paramodulation, Inf. Comput, vol.147, issue.1, pp.1-21, 1998.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann

, J. ACM, vol.53, issue.6, pp.937-977, 2006.

R. Nieuwenhuis and A. Rubio, Paramodulation-based theorem proving, Handbook of Automated Reasoning, vol.1, pp.371-443, 2001.

D. C. Oppen, Complexity, convexity and combinations of theories. Theor. Comput. Sci, vol.12, pp.291-302, 1980.

D. A. Plaisted, Equational reasoning and term rewriting systems, Handbook of Logic in Artificial Intelligence and Logic Programming, vol.I, pp.273-364, 1993.

D. A. Plaisted, Automated theorem proving, Wiley Interdisc. Rev. Cog. Sci, vol.5, issue.2, pp.115-128, 2014.

S. Ranise, C. Ringeissen, and C. G. Zarba, Combining data structures with nonstably infinite theories using many-sorted logic, Proc. of FroCoS-5, vol.3717, pp.48-64, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000570

G. Reger, M. Suda, and A. Voronkov, Playing with AVATAR, Proc. of CADE-25, vol.9195, pp.399-415

. Springer, , 2015.

C. Ringeissen, Cooperation of decision procedures for the satisfiability problem, Proc. of FroCoS-1, Applied Logic, pp.121-140, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073939

C. Ringeissen and V. Senni, Modular termination and combinability for superposition modulo counter arithmetic, Proc. of FroCoS-8, vol.6989, pp.211-226, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00636589

G. A. Robinson and L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Machine Intelligence, vol.4, pp.135-150, 1969.

M. Rusinowitch, Theorem-proving with resolution and superposition, J. Symb. Comput, vol.11, issue.1 & 2, pp.21-50, 1991.

S. Schulz, System description: E 1.8, Proc. of LPAR-19, vol.8312, pp.735-743

. Springer, , 2013.

R. Sebastiani, Lazy satisfiability modulo theories, J. Satisfiability Bool. Model. and Comput, vol.3, pp.141-224, 2007.

N. Shankar, Automated deduction for verification, ACM Comput. Surv, vol.41, issue.4, pp.40-96, 2009.

R. E. Shostak, An algorithm for reasoning about equality, Commun. ACM, vol.21, issue.7, pp.583-585, 1978.

V. Sofronie-stokkermans, Locality results for certain extensions of theories with bridging functions, Proc. of CADE-22, vol.5663, pp.67-83, 2009.

C. Tinelli and M. T. Harandi, A new correctness proof of the Nelson-Oppen combination procedure, Proc. of FroCoS-1, Applied Logic, pp.103-120, 1996.

C. Tinelli and C. Ringeissen, Unions of non-disjoint theories and combinations of satisfiability procedures, Theor. Comput. Sci, vol.290, issue.1, pp.291-353, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099668

C. Tinelli and C. G. Zarba, Combining decision procedures for sorted theories, Proc. of JELIA-9, vol.3229, pp.641-653, 2004.

C. Tinelli and C. G. Zarba, Combining non-stably infinite theories, J. Automat. Reason, vol.34, issue.3, pp.209-238, 2005.

C. Wang, F. Ivan?i?, M. Ganai, and A. Gupta, Deciding separation logic formulae by SAT and incremental negative cycle elimination, Proc. of LPAR-12, vol.3835, pp.322-336

. Springer, , 2005.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., Spass version 3.5, Proc. of CADE-22, vol.5663, pp.140-145, 2009.

T. Wies, R. Piskac, and V. Kuncak, Combining theories with shared set operations, Proc. of FroCoS-7, vol.5749, pp.366-382, 2009.

S. A. Wolfman and D. S. Weld, The LPSAT engine and its application to resource planning, Proc. of IJCAI-16, vol.1, pp.310-316, 1999.

A. Zelji?, C. M. Wintersteiger, and P. Rümmer, Deciding bit-vector formulas with mcSAT, Proc. of SAT-19, vol.9710, pp.249-266, 2016.