Rewrite-based decision procedures

The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that the considered inference system generates finitely many clauses from the presentation T of a theory and a finite set of ground unit clauses, then any fair strategy can be used as a T-satisfiability procedure. This approach makes it conceptually simple to combine several theories, under the variable-inactive condition. In this paper, we introduce sufficient conditions to generalize the entire framework of rewrite-based T-satisfiability procedures to rewrite-based T-decision procedures. These conditions, collectively termed as subterm-inactivity, will allow us to obtain rewrite-based T-decision procedures for several theories, namely those of equality with uninterpreted functions, arrays with or without extensionality and two of its extensions, finite sets with extensionality and recursive data structures. We show that subterm-inactive theories are also variable-inactive, and can therefore all be combined.