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

Thery's implementation provides some standard optimizations that we do not
include. Regarding future work, we are interested in studying how our verified
implementation could be improved to incorporate some of the refinements built
into the very specialized and optimized (and not formally verified) versions used
in industrial-strength applications. It would be also interesting to use it to verify
some application of Grobner bases such as those described in [2].
An obvious improvement in the verified implementation is to avoid the “type
conditions” in the body of Buchberger-aux , since these conditions are unnec-
essarily evaluated in every recursive call. But these conditions are needed to
ensure termination. Until Acl2 version 2.7, there was no way to avoid this; but
since the recent advent of Acl2 version 2.8 that is no longer true, since it is
possible for a function to have two different bodies, one used for execution and
another for its logical definition: this is done by previously proving that both
bodies behave in the same way on the intended domain of the function. We plan
to apply this new feature to our definition of Buchberger's algorithm.

References

1.Baader,F.&Nipkow,T.: Term Rewriting and All That. Cambridge University
Press (1998)
2. Buchberger, B. & Winkler, F. (eds.): Grobner Bases and Applications. London
Mathematical Society Series 251 (1998)
3. Coquand, T. & Persson, H.: Grobner Bases in Type Theory. Types for Proofs and
Programs, International Workshop. LNCS :33-46 (1999)

4. Geddes, K. O.; Czapor, S. R. & Labahn, G.: Algorithms for Computer Algebra.
Kluwer (1998)
5. Kaufmann, M.; Manolios, P. & Moore, J S.: Computer-Aided Reasoning: An Ap-
proach. Kluwer (2000)
6. Kaufmann, M. & Moore, J S.: Structured Theory Development for a Mechanized
Logic. Journal of Automated Reasoning

1657

(2):161-203 (2001)
7. Martın, F. J.; Alonso, J. A.; Hidalgo, M. J. & Ruiz, J. L.: A Formal Proof of
Dickson's Lemma in ACL2. Logic for Programming, Artificial Intelligence and
Reasoning. LNAI 2850 :49-58 (2003)
8. Medina,I.;Alonso,J.A.&Palomo,F.: Automatic Verification of Polynomial Rings
Fundamental Properties in ACL2. ACL2 Workshop 2000. Department of Computer
Sciences, University of Texas at Austin. TR-00-29 (2000)
9. Medina,I.;Palomo,F.&Alonso,J.A.: Implementation in ACL2 of Well-Founded
Polynomial Orderings. ACL2 Workshop 2002 (2002)
10. Rudnicki, P.; Schwarzweller, C. & Trybulec, A.: Commutative Algebra in the Mizar
System. Journal of Symbolic Computation 32 (1-2):143-169 (2001)
11. Ruiz, J. L.; Alonso, J. A.; Hidalgo, M. J. & Mart ın, F. J.: Formal Proofs about
Rewriting using ACL2. Annals of Mathematics and Artificial Intelligence 36 (3):
239-262 (2002)
12. Sustyk, M.: Proof of Dickson's Lemma Using the ACL2 Theorem Prover via an
Explicit Ordinal Mapping. Fourth International Workshop on the ACL2 Theorem
Prover and Its Applications (2003)
13. Thery, L.: A Machine-Checked Implementation of Buchberger's Algorithm. Journal
of Automated Reasoning 26 (2): 107-137 (2001)

26