Quantoren Elimination
Z0
R
R
R
R
R
Z1
f
f
f
f
f
...
f
f
f
...
I
I
$x.B
B open
$x.L1Ù... Ù Ln
Û
Li atomic
$x.Lk+1Ù... Ù Ln
xÏFV(Li)
L1Ù... Ù Lk
Û
xÎFV(Li)
Ù
true
false
Ù
...
Ù
...
Jeder atomare Ausdruck über
W enthält höchstens eine freie Variable !!
2. W gestattet Quantoren-Elimination, d.h. jeder
Ausdruck ist äquivalent zu einem offenen Ausdruck.
Vorherige Folie
Nächste Folie
Zurück zur ersten Folie
Graphik-Version anzeigen