Verified Computer Algebra in ACL2 - Artificial Intelligence and Symbolic Computation - page 178

(defthm |nf(p, F) = red*(p, F)|
(implies (and (k-polynomialp p) (k-polynomialsp F))
(equal (nf p F) (red* p F))))

With this result, we can translate all the properties proved about nf to red* .
This is typical in our formalization: we use some functions for reasoning, and
other functions for computing, translating the properties from one to another by
proving equivalence theorems. For example, we proved the stability of the ideal
with respect to red* using this technique.

5Grobner Bases

The computation of normal forms with respect to a given ideal can be seen as a
generalized polynomial division algorithm, and the normal form computed as the
“remainder” of that division. The ideal membership problem can be solved taking
this into account: compute the normal form and check for the zero polynomial.
Unfortunately, it is possible that, for a given basis F , a polynomial in

cannot
be reduced to the zero polynomial. This is where Grobner bases come into play:

F

Definition 6. G is a Grobner basis of the ideal generated by F if G = F

and p ∈G⇐⇒p → ∗ G 0 .

The key point in Buchberger's algorithm is that the property of being a
Grobner basis can be deduced by only checking that a finite number of polyno-
mials (called s-polynomials ) are reduced to zero:

Definition 7. Let p and q be polynomials. Let m , m 1 and m 2 be monomials such
that m =lcm( lm ( p ) , lm ( q )) and m 1 · lm ( q ) . The s-polynomial

induced by p and q is defined as s-poly ( p, q )= m 1 · p − m 2 · q

lm ( p )= m = m 2 ·

→ F

Theorem 1. Let Φ ( F ) ≡∀p, q ∈ F s-poly ( p, q ) 0 . The reduction induced

by F is locally confluent if Φ ( F ) is verified. That is:

⇒∃s ( p → F s ∧ q → F s )) Φ ( F )= ⇒∀p, q, r ( r → F p ∧ r → F q =

This theorem was the most dicult to formalize and prove in our work. First,
note that it cannot be stated as a single theorem in the quantifier-free Acl2 logic,
due to the universal quantifier in its hypothesis, Φ ( F ). For this reason, we state
its hypothesis by the following encapsulate (we omit the local witnesses and
some nonessential technical details):

(encapsulate
((F () t) (s-polynomial-proof (p q) t))
···
(defthm |Phi(F)|
(let ((proof (s-polynomial-proof p q)))
(and (k-polynomials (F))
(implies (and (in<> p (F)) (in<> q (F)))
(->* (s-poly p q) (|0|) proof (F)))))