\newcommand{\RR}{\mathbb{R}}


\begin{slide}{(Un)Gl. zwischen Polynomen}

Erweiterung der Syntax:
\begin{itemize}
\item Summand $\to$ Zahl ($\cdot$ Variable)$^*$
\end{itemize}

das aus der Schule bekannte \glqq Lösen quadratischer Gleichungen\grqq\
ist Quantor-Elimination:

$(\exists x: x^2 -x +a\le 0) \iff (a \le 1/4)$.

in mehreren Variablen? --- Für Struktur $\RR$ entscheidbar
\begin{itemize}
\item Gleichungen: Gröbnerbasen
\item Ungleichungen: Alfred Tarksi, QEPCAD,
\end{itemize}
aber für $\ZZ$ nicht! (Juri Matiasevitch, Julia Robinson)

\end{slide}
