Nelson-Oppen (I)

(Wdhlg) Formel/Ausdruck

purification (Reinigung):

• durch Einführen neuer Variablen:
• alle atomaren Formeln enthalten nur Ausdrücke einer Theorie

Beispiel:

• vorher: φ : = x₁≤f (x₁) mathend000#
• nachher: φ' : = x₁≤a∧a = f (x₁) mathend000#

im Allg. φ$\iff$∃a,… : φ' mathend000#

d. h. φ mathend000# erfüllbar $\iff$ mathend000# φ' mathend000# erfüllbar.