\begin{slide}{Fourier-Motzkin-Verfahren}

Def.: eine Ungls. ist in $x$-Normalform, wenn jede Ungl.
\begin{itemize} \itemsep 0pt
\item die Form \glqq $x$ ($\le \;\mid\; \ge$) (Ausdruck ohne $x$)\grqq\ hat
\item oder $x$ nicht enthält.
\end{itemize}

Satz: jedes Ungls. besitzt äquivalente $x$-Normalform.

\bigskip
Def: für Ungls. $U$ in $x$-Normalform: 

$U_x^\downarrow := \{ A \mid (x\ge A) \in U\},~
U_x^\uparrow := \{ B \mid (x\le B) \in U\},$ 

$U_x^- = \{ C \mid C\in U, \text{$C$ enthält $x$ nicht} \}.$

\bigskip
Def: ($x$-Eliminations-Schritt) für $U$ in $x$-Normalform:

$U \to_x  \{ A \le B \mid A\in U_x^\downarrow, B\in U_x^\uparrow \}  \cup U_x^-$

\bigskip
Satz: ($U$ erfüllbar und $U\to_x V$) $\iff$ ($V$ erfüllbar).

\bigskip FM-Verfahren: Variablen nacheinander eliminieren.

\end{slide}
