Anwendung: Idealmitgliedschaft

automatisches Beweisen von Behauptungen der Form:

Wenn p₁(x₁,...) = 0 $\wedge$ $\wedge$ p_n(x₁,...) = 0, dann q(x₁,...) = 0.

äquivalent: q $\in$ Ideal(p₁,..., p_n).

äquivalent: es gibt kein (x₁,...) mit p₁(x₁,...) = 0 $\wedge$ $\wedge$ p_n(x₁,...) = 0 $\wedge$ q(x₁,...) $\neq$ 0.

äquivalent (Rabinowitsch-Trick): es gibt kein (x₁,...) mit p₁(x₁,...) = 0 $\wedge$ $\wedge$ p_n(x₁,...) = 0 $\wedge$ 1 - f ^. q(x₁,...) = 0.

äquivalent: Gröbnerbasis dieser Polynome ist {1}, d. h. das Ideal besteht aus allen Polynomen.

Vgl. Resolution in der Logik: Falls (A₁ $\wedge$...$\wedge$ A_n $\wedge$ $\notB$) widersprüchlich, dann (A₁ $\wedge$...$\wedge$ A_n$\implies$B); und: aus widersprüchlicher Formel(menge) folgt jede Formel.