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)