Verfahren nach Fourier und Motzkin (I)

transformiert ein lin. Unglsys. in ein erfüllbarkeitsäquivalentes mit einer Variablen weniger.

Beispiel: aus (x + y$ \le$1 $ \wedge$ 2x + 3y$ \ge$0) wird (y$ \ge$ - 2)

Das ist (wie schon Gauß für Gleichungssyst.) ein Verfahren zur Quantor-Elimination

($ \exists$x, y : x + y$ \le$1 $ \wedge$ 2x + 3y$ \ge$0)$ \iff$($ \exists$y : y$ \ge$ - 2)



2009-06-22