- 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 Fourth Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR)*,*Third International Joint Conference on Automated Resoning (IJCAR)*and*Fourth 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 Fifth 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 (a long version of the presentation was given as a rehearsal talk in Verona: Slides). - 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
*Notes of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), Seventeenth International Conference on Computer Aided Verification (CAV)*, 33-41, Edinburgh, Scotland, UK, July 2005 (preliminary work was presented as an invited talk at the Third 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
*Notes of the Fifth Workshop on the Implementation of Logics (IWIL), Eleventh 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
*Notes of the Second Workshop on Verification (VERIFY), Third 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).

With Silvio Ghilardi, Enrica Nicolini, Silvio Ranise and Daniele Zucchelli,
I worked on decidability and undecidability results in combination of theories
by equality sharing (the Nelson-Oppen scheme) and by first-order inferences,
also showing that *variable inactive* theories are *stably infinite*:

- 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 Third Internationl Joint Conference on Automated Resoning (IJCAR)*,*Fourth 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.

With Mnacho Echenim I generalized this approach to deciding
whether an arbitrary quantifier-free formula (or equivalently a set of ground clauses)
is *T*-satisfiable.
This result covers the theories of *equality*,
*lists* (whether non-empty or possibly empty, possibly cyclic or acyclic),
*arrays*, *finite sets* and *records*
(all three of them with or without extensionality),
*integer offsets* (whether modulo or not), and
*recursive data structures* as well as any of their combinations.
Furthermore, we obtained *polynomial* rewrite-based *T*-satisfiability procedures
for the theories of *records with extensionality* and *integer offsets*:

- 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*Notes of the First Workshop on Automated Deduction: Decidability, Complexity, Tractability (ADDCT), Twenty-first 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 Sixth Workshop on Strategies in Automated Deduction (STRATEGIES)*,*Third International Joint Conference on Automated Resoning (IJCAR)*and*Fourth 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.

An alternative approach is to *decompose* the problem
in such a way that it can be solved by invoking first a first-order
prover as preprocessor and then 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 Twenty-first 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.