mathend000#-Normalform, wenn jede Ungl.
- die Form „x
mathend000# (
≤ | ≥
mathend000#) (Ausdruck ohne x
mathend000#)`` hat
- oder x
mathend000# nicht enthält.
Satz: jedes Ungls. besitzt äquivalente x
mathend000#-Normalform.
Def: für Ungls. U
mathend000# in x
mathend000#-Normalform:
Ux↓ : = {A | (x≥A)∈U}, Ux↑ : = {B | (x≤B)∈U},
mathend000#
Ux- = {C | C∈U,$C$ enthält $x$ nicht}.
mathend000#
Def: (x
mathend000#-Eliminations-Schritt) für U
mathend000# in x
mathend000#-Normalform:
U→x{A≤B | A∈Ux↓, B∈Ux↑}∪Ux-
mathend000#
Satz: (U
mathend000# erfüllbar und U→xV
mathend000#)
mathend000# (V
mathend000# erfüllbar).
FM-Verfahren: Variablen nacheinander eliminieren.
2014-03-31