Motivation (I): Polynom-Interpretationen

• Anwendung: wfmA A = ($\mathbb {N}$, > ,[⋅]), jedes [f]_A ist Polynom.

  Bsp: [f](x, y) = x²⋅y (Vorsicht), [g](x, y) = x² + y

  Bsp: kompatibel mit g(g(x, y), z)→g(x, g(y, z))?

• es müssen Aussagen der Form ∀x, y, z : P(x, y, z) > 0 (automatisch) nachgewiesen werden
• welche Approximation in der autotool-Aufgabe dazu?
• Zeige x, y≥0⇒(x + y)/2≥$\sqrt[2]{{xy}}$

  Ü: Zeige x, y, z≥0⇒(x + y + z)/3≥$\sqrt[3]{{xyz}}$

  Ü: Hilberts 17. Problem (nichtneg. P, das kein SOS ist)