(Wdhlg) Formel/Ausdruck
purification (Reinigung):
- durch Einführen neuer Variablen:
- alle atomaren Formeln
enthalten nur Ausdrücke einer Theorie
Beispiel:
- vorher:
φ : = x1≤f (x1)
mathend000#
- nachher:
φ' : = x1≤a∧a = f (x1)
mathend000#
im Allg.
φ∃a,… : φ'
mathend000#
d. h. φ
mathend000# erfüllbar
mathend000# φ'
mathend000# erfüllbar.
2014-03-31