Superposition-based decision procedures
Given a theory T, consider the problem of deciding
whether a set of ground literals is T-satisfiable.
In order to apply a complete theorem-proving method,
the key step is to prove termination.
Alessandro Armando, Silvio Ranise and Michaël Rusinowitch did it
for a standard superposition-based inference system and the theories of
arrays (with or without extensionality),
non-empty (possibly cyclic) lists,
finite sets and the combination of arrays and non-empty lists.
With Alessandro Armando, Silvio Ranise and Stephan Schulz,
I added the theories of records (with or without extensionality),
integer offsets, integer offsets modulo and
possibly empty (possibly cyclic) lists;
and with Mnacho Echenim that of
recursive data structures with one constructor and any number of selectors,
which includes integer offsets and acyclic non-empty lists
as special cases.
With Alessandro Armando, Silvio Ranise and Stephan Schulz,
I obtained a modularity theorem showing termination in a union of
variable-inactive theories, given termination for each of them.
All above mentioned theories are variable-inactive.
An experimental comparison of the
E theorem prover with the CVC (Cooperating Validity Checker) and
CVC Lite validity checkers completed the work:
- 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:
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