(Un)Gl. zwischen Polynomen

Erweiterung der Syntax:

• Summand $\to$ Zahl ( ^. Variable)^*

das aus der Schule bekannte ,,Lösen quadratischer Gleichungen`` ist Quantor-Elimination:

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

in mehreren Variablen? -- Für Struktur $\mathbb {R}$ entscheidbar

• Gleichungen: Gröbnerbasen
• Ungleichungen: Alfred Tarksi, QEPCAD,

aber für $\mathbb {Z}$ nicht! (Juri Matiasevitch, Julia Robinson)