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

The first line of this encapsulate presents the signature of the functions it in-
troduces, and the theorem inside can be seen as an assumed property about these
functions. In this case, we are assuming that we have a list of polynomials given
by the 0-ary function F , with the property that every s-polynomial formed with
pairs of elements of (F) is reduced to (|0|) . This reduction is justified by a func-
tion s-polynomial-proof computing the corresponding sequence of proof steps
representing the reduction to (|0|) . We insist that F and s-polynomial-proof
are not completely defined: we are only assuming |Phi(F)| about them.
Now, the conclusion of Th. 1 is established as follows:
(defthm |Phi(F) => local-confluence(->F)|
(let ((proof2 (transform-local-peak-F proof1)))
(implies (and (k-polynomial p) (k-polynomial q)
(<->* p q proof1 (F)) (local-peakp proof1))
(and (<->* p q proof2 (F)) (valleyp proof2)))))
This theorem needs some explanation. Note that local confluence can be
reformulated in terms of the “shape” of the involved proofs: a reduction is
locally confluent if, and only if, for every local peak proof (that is, of the
form p ← r → q ) there exists an equivalent valley proof (that is, of the form

→ s ∗

∗

p ← q ). It is easy to define in Acl2 the functions local-peakp and valleyp ,

checking those shapes of proofs. Note that again due to the absence of existen-
tial quantification, the valley proof in the above theorem is given by a function
transform-local-peak-F , such that from a given local peak proof, it computes
an equivalent valley proof. The definition of this function is very long and follows
the same case distinction as in the classical proof of this result; only in one of
its cases (the one dealing with “overlaps”), s-polynomial-proof is used as an
auxiliary function, reflecting in this way where the assumption about Φ ( F )is

necessary.
The last step in this section follows from general results of abstract reduction
relations. In particular, if a reduction is locally confluent and Noetherian then
its induced equivalence can be decided by checking if normal forms are equal.
This has been proved in Acl2 [11] as a consequence of Newman's lemma, also
proved there. We can reuse this general result by functional instantiation and
obtain an Acl2 proof of the fact that, if Φ ( F ), p

∗
↔ F q ⇐⇒

nf F ( p )= nf F ( q ).

and red F ,andthe With this result, and using the equality between nf F

≡ F and ↔ F , it can be easily deduced that if Φ ( F )then F

equality between is

aGrobner basis (of ). This is established by the following theorem (notice

that (F) is still the list of polynomials assumed to have property Φ by the above
encapsulate ):
(defthm |Phi(F) => (p in <F> <=> red*(p, F) = 0)|
(implies (k-polynomial p)
(iff (in<> p (F)) (equal (red* p (F)) (|0|)))))

F

6 Buchberger's Algorithm
Buchberger's algorithm obtains a Grobner basis of a given finite set of polyno-
mials F

by the following procedure: if there is a s-polynomial of F such that its