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:

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:

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:

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