Abstract
We present an implementation of Buchberger's algorithm that has been proved correct within the proof assistant Coq. The implementation contains the basic algorithm plus two standard optimizations.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Bauer, A., Clarke, E. and Zhao, X.: Analytica-an experiment in combining theorem proving and symbolic computation, J. Automated Reasoning 21(3) (1998), 295–325.
Bertot, Y. and Bertot, J.: CtCoq: A system presentation, in Automated Deduction-CADE-13, Lecture Notes in Artif. Intell. 1104, Springer-Verlag, 1996.
Buchberger, B.: Introduction to Gröbner bases, in B. Buchberger and F.Winkler (eds.), Gröbner Bases and Applications, Cambridge University Press, 1998, pp. 3–31.
Buchberger, B., Jebelean, T., Kriftner, F., Marin, M., Tomuta, E. and Vasaru, D.: A survey on the theorema project, in International Symposium on Symbolic and Algebraic Computation (ISSAC'97), ACM, 1997.
Calmet, J. and Homann, K.: Classification of communication and cooperation mechanisms for logical and symbolic computation systems, in First International Workshop 'Frontiers of Combining Systems' (FroCoS'96), Kluwer Series on Appl. Logic, Springer-Verlag, 1996, pp. 133–146.
Constable, R. L.: Expressing computational complexity in constructive type theory, in International Workshop on Logic and Computational Complexity, Lecture Notes in Artif. Intell. 960, Springer-Verlag, July 1994.
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T. and Smith, S. F.: Implementing Mathematics with Nuprl Proof Development System, Prentice-Hall, 1986.
Coquand, T. and Persson, H.: Gröbner bases and type theory, in T. Altenkirch, W. Naraschewski, and B. Reus (eds.), Types for Proofs and Programs, Lecture Notes in Comput. Sci. 1657, Springer-Verlag, 1999.
Coscoy, Y., Kahn, G. and Théry, L.: Extracting text from proofs, in Typed Lambda Calculus and Its Applications, Lecture Notes in Comput. Sci. 902, Springer-Verlag, 1995, pp. 109–123.
Farmer, W. M., Guttman, J. D. and Thayer, F. J.: Little theories, in D. Kapur (ed.), Automated Deduction-CADE-11, Lecture Notes in Comput. Sci. 607, Springer-Verlag, 1992, pp. 567–581.
Geddes, K. O., Czapor, S. R. and Labahn, G.: Algorithms for Computer Algebra, Kluwer Acad. Publ., 1992.
Gordon, M. and Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge Univ. Press, 1993.
Harrison, J. R.: Theorem Proving with the Real Numbers, Springer-Verlag, 1998.
Harrison, J. R. and Théry, L.: A skeptic's approach to combining HOL and Maple, J. Automated Reasoning 21(3) (1998), 295–325.
Huet, G., Kahn, G. and Paulin-Mohring, C.: The Coq proof assistant: A tutorial: Version 6.1, Technical Report 204, INRIA, 1997.
Jackson, P. B.: Enhancing the Nuprl proof development system and applying it to computational abstract algebra, Technical Report TR95–1509, Cornell University, 1995.
Knuth, D. E. and Bendix, P. B: Simple word problems in universal algebras, in J. Leech (ed.), Computational Problems in Abstract Algebras, Pergamon Press, 1970.
Ménissier-Morain, V.: The CAML numbers reference manual, Technical Report 141, INRIA, 1992.
Nederpelt, R. P., Geuvers, J. H. and De Vrijer, R. C. (eds.): Selected Papers on Automath, North-Holland, 1994.
Paulin-Mohring, C. and Werner, B.: Synthesis of ML programs in the system Coq, J. Symbolic Comput. 15(5–6) (1993), 607–640.
Paulson, L. C.: Constructing recursion operators in intuitionistic type theory, J. Symbolic Comput. 2(4) (1986), 325–355.
Paulson, L. C.: Isabelle: A Generic Theorem Prover, Lecture Notes in Comput. Sci. 828, Springer-Verlag, 1994.
Pottier, L.: Dickson's lemma, Available at ftp://ftp-sop.inria.fr/lemme/Loic.Pottier/ MON/, 1996.
Rudnicki, P.: An overview of the MIZAR projet, in Workshop on Types and Proofs for Programs, Available by ftp at pub/cs-reports/baastad.92/proc.ps.Z on ftp.cs.chalmers.se, 1992.
Rushby, J. M., Shankar, N. and Srivas, M.: PVS: Combining specification, proof checking, and model checking, in CAV '96, Lecture Notes in Comput. Sci. 1102, Springer-Verlag, July 1996.
Schwarzweller, C.: Mizar verification of generic algebraic algorithms, Ph.D. Thesis, Wilhelm-Schickard Institute for Computer Science, University of Tübingen, 1997.
Théry, L.: A certified version of Buchberger's algorithm, in Automated Deduction-CADE-15, Lecture Notes in Artif. Intell. 1421, Springer-Verlag, 1998, pp. 349–364.
Vega, G. P. and Werner, B.: Personal communication, 1998.
Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer, Addison-Wesley, 1988.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Théry, L. A Machine-Checked Implementation of Buchberger's Algorithm. Journal of Automated Reasoning 26, 107–137 (2001). https://doi.org/10.1023/A:1026518331905
Issue Date:
DOI: https://doi.org/10.1023/A:1026518331905