SMT in theory union and superposition-based decision procedures
Satisfiability modulo theories (SMT) is the problem of deciding
whether a quantifier-free formula is T-satisfiable.
This problem is especially important when T is a union of theories:
Superposition-based strategies decide the T-satisfiability of sets
of ground literals in several theories of data structures,
and, thanks to a modularity theorem, in their unions:
- 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:
Ideas and results from some of these papers were presented in a colloquium given at the Department of Mathematical Sciences, Tsinghua University, Beijing, PR China, in May 2007:
Slides.
Maria Paola Bonacina