Decision procedures for variable-inactive theories and two polynomial T-satisfiability procedures (Position paper)

Most reasoning-based verification systems rely on T-decision procedures for the validity of ground formulae modulo a background theory T. Since most problems involve multiple theories, the ability to reason in combinations of theories is crucial. The rewrite-based approach to T-satisfiability applies directly an inference system for FOL+=. The approach is uniform, because the presentation of the theory is part of the input, and modular, because if the theorem-proving strategy is a T_i-satisfiability procedure for T_1,...,T_n, it is also a satisfiability procedure for their union, provided the component theories are variable-inactive. A first contribution of this paper is to show how to derive polynomial T-satisfiability procedures for the theories of integer offsets and records with extensionality. A second contribution of this paper is a generalization of the rewrite-based approach from sets of literals to sets of clauses.