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:

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

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):

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