Nelson-Oppen Restrictions (Satisfiability Modulo Theory)

Definition

Nelson-Oppen Restrictions (Satisfiability Modulo Theory)

The standard Nelson–Oppen decision procedure combines theories ${\mathcal{T}}_1,\dots ,{\mathcal{T}}_n$ only under the following restrictions:

1. Decidable quantifier-free conjunctive fragments: for every $i$, satisfiability modulo ${\mathcal{T}}_i$ is decidable for quantifier-free conjunctions of literals;
2. Disjoint signatures: the non-logical function and predicate symbols of the signatures are pairwise disjoint, $$i\ne j⟹({\mathcal{F}}_i\cup {\mathcal{P}}_i)\cap ({\mathcal{F}}_j\cup {\mathcal{P}}_j)=\varnothing ,$$ apart from built-in equality; shared sorts and variables are permitted;
3. Stable infiniteness: every ${\mathcal{T}}_i$ is a stably infinite theory.

Under these conditions, purified component constraints can be decided separately and combined by communicating equalities over their shared variables. Stable infiniteness ensures that locally satisfying models can be given compatible domains.