Decision procedures by theory decomposition

An alternative approach to purely rewrite-based T-decision procedures enables us to obtain T-decision procedures by combining a rewrite-based first-order prover and an SMT-solver, in such a way to unite their respective strengths: reasoning with quantifiers and equality for the rewrite-based prover, reasoning with propositional logic and special theories, such as linear arithmetic, for the SMT-solver. In this approach, the T-decision problem is decomposed and the rewrite-based prover and SMT-solver are pipelined, in such a way that the rewrite-based prover is invoked only once as a preprocessor for the SMT-solver:

Maria Paola Bonacina and Mnacho Echenim. Theory decision by decomposition. Journal of Symbolic Computation, 45(2):229-260, February 2010; DOI: 10.1016/j.jsc.2008.10.008.
Maria Paola Bonacina and Mnacho Echenim. T-decision by decomposition. In Proceedings of the Twenty-first International Conference on Automated Deduction (CADE), Bremen, Germany, July 2007. Springer, Lecture Notes in Artificial Intelligence 4603, 199-214, 2007.

Maria Paola Bonacina