Model-theoretic methods in combined constraint satisfiability (Q556677)

The Nelson-Oppen combination procedure is extended to the case of two theories over non-disjoint signatures, in the presence of compatibility conditions over a common universal subtheory \(T_0\). The extension gives combined decidability in case \(T_0\) is locally finite. If \(T_0\) is not locally finite then the method can be used to limit residue exchange or to forbid impure inferences in saturation-based theorem proving.