We extend the Nelson–Oppen combination procedure to the case of theories that are compatible with respect to a common subtheory in the shared signature. The notion of compatibility relies on model completions and related concepts from classical model theory.
Keywords combination - Nelson–Oppen procedure - fusion - superposition calculus - quantifier elimination - model completions