Nelson-Oppen (I)

(Wdhlg) Formel/Ausdruck

purification (Reinigung):

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

Beispiel:

• vorher: $\phi$ : = x₁$\le$f (x₁)
• nachher: $\phi{^\prime}$ : = x₁$\le$a $\wedge$ a = f (x₁)

im Allg. $\phi$$\iff$$\exists$a,...: $\phi{^\prime}$

d. h. $\phi$ erfüllbar $\iff$ $\phi{^\prime}$ erfüllbar.