- Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, and Cesare Tinelli.
Theory combination: beyond equality sharing.
In
*Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader*. Springer, Lecture Notes in Artificial Intelligence 11560, 57-89, June 2019 (**invited**); DOI: 10.1007/978-3-030-22102-7_3.

- Alessandro Armando, Maria Paola Bonacina, Silvio Ranise and Stephan Schulz.
New results on rewrite-based satisfiability procedures.
ACM Transactions on Computational Logic,
10(1):129-179, January 2009;
DOI: 10.1145/1459010.1459014
(archived in CoRR as arXiv:cs/0604054v4).
- Maria Paola Bonacina and Mnacho Echenim.
Rewrite-based satisfiability procedures for recursive data structures.
In
*Proceedings of the 4th Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR)*satellite of the*3rd International Joint Conference on Automated Resoning (IJCAR)*held at the*4th Federated Logic Conference (FLoC)*, Seattle, WA, USA, August 2006. Elsevier, Electronic Notes in Theoretical Computer Science 174(8):55-70, June 2007; DOI: 10.1016/j.entcs.2006.11.039. - Alessandro Armando, Maria Paola Bonacina, Silvio Ranise and Stephan Schulz.
On a rewriting approach to satisfiability procedures:
extension, combination of theories and an experimental appraisal.
In
*Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS)*, Vienna, Austria, September 2005. Springer, Lecture Notes in Artificial Intelligence 3717, 65-80, 2005; DOI: 10.1007/11559306_4. - Alessandro Armando, Maria Paola Bonacina, Silvio Ranise and Stephan Schulz.
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedures.
In
*Proceedings of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR)*satellite of the*17th International Conference on Computer Aided Verification (CAV)*, 33-41, Edinburgh, Scotland, UK, July 2005 (preliminary work was presented as an invited talk at the 3rd KeY Symposium, Adam-Stegerwald-Haus, Königswinter, Germany, June 2004: Slides). - Stephan Schulz and Maria Paola Bonacina.
On handling distinct objects in the superposition calculus.
In
*Proceedings of the 5th Workshop on the Implementation of Logics (IWIL)*satellite of the*11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)*, 66-77, Montevideo, Uruguay, March 2005. - Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Michaël
Rusinowitch and Aditya Kumar Sehgal.
High-performance deduction for verification: a case study in the theory of arrays.
In
*Proceedings of the 2nd Workshop on Verification (VERIFY)*satellite of the*18th International Conference on Automated Deduction (CADE)*held at the*3rd Federated Logic Conference (FLoC)*, Technical Report 07/2002, DIKU, University of Copenhagen, pages 103-112, Copenhagen, Denmark, July 2002 (later presented at the Dagstuhl Seminar 03171 on Deduction and Infinite State Model Checking, April 2003: Slides).

This work opened the way to understand the relationship between superposition and the equality-sharing (aka Nelson-Oppen) scheme for combination of theories:

- Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise and
Daniele Zucchelli.
Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures.
In
*Proceedings of the 3rd Internationl Joint Conference on Automated Resoning (IJCAR)*, held at the*4th Federated Logic Conference (FLoC)*, Seattle, WA, USA, August 2006. Springer, Lecture Notes in Artificial Intelligence 4130, 513-527, 2006; DOI: 10.1007/11814771_42. - Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise and Daniele Zucchelli. Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. Internal Report No. 308-06, Dipartimento di Scienze dell'Informazione, Università degli Studi di Milano, May 2006, 1-20.

For the theories covered by the modularity theorem,
superposition-based strategies also decide the more general problem of the
*T*-satisfiability of an arbitrary quantifier-free formula
(or equivalently a set of ground clauses):

- Maria Paola Bonacina and Mnacho Echenim.
On variable-inactivity and polynomial
*T*-satisfiability procedures. Journal of Logic and Computation, 18(1):77-96, February 2008; DOI: 10.1093/logcom/exm055. - Maria Paola Bonacina and Mnacho Echenim.
Decision procedures for variable-inactive theories and
two polynomial
*T*-satisfiability procedures (Position paper). In*Proceedings of the 1st Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT)*satellite of the*21st International Conference on Automated Deduction (CADE)*, 65-67, Bremen, Germany, July 2007. - Maria Paola Bonacina and Mnacho Echenim.
Rewrite-based decision procedures.
In
*Proceedings of the 6th Workshop on Strategies in Automated Deduction (STRATEGIES)*satellite of the*3rd International Joint Conference on Automated Resoning (IJCAR)*held at the*4th Federated Logic Conference (FLoC)*, Seattle, WA, USA, August 2006. Elsevier, Electronic Notes in Theoretical Computer Science 174(11):27-45, July 2007; DOI: 10.1016/j.entcs.2006.11.042. - Maria Paola Bonacina and Mnacho Echenim. Generic theorem proving for decision procedures, Research Report RR 41/2006, Dipartimento di Informatica, Università degli Studi di Verona, August 2006, revised March 2007.

A superposition-based strategy can also act as a preprocessor for an 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 21st International Conference on Automated Deduction (CADE)*, Bremen, Germany, July 2007. Springer, Lecture Notes in Artificial Intelligence 4603, 199-214, 2007; DOI: 10.1007/978-3-540-73595-3_14.