Knuth-Bendix procedure and Buchberger algorithm: a synthesis

ABSTRACT

The Knuth-Bendix procedure for the completion of a rewrite rule system and the Buchberger algorithm for computing a Gröbner basis of a polynomial ideal are very similar in two respects: they both start with an arbitrary specification of an algebraic structure (axioms for an equational theory and a basis for a polynomial ideal, respectively) which is transformed to a very special specification of this algebraic structure (a complete rewrite rule system and a Gröbner basis of the polynomial ideal, respectively). This special specification allows to decide many problems concerning the given algebraic structure. Moreover, both algorithms achieve their goals by employing the same basic concepts: formation of critical pairs and completion. Although the two methods are obviously related, the exact nature of this relation remains to be clarified. Based on previous work we show how the Knuth-Bendix procedure and the Buchberger algorithm can be seen as special cases of a more general completion procedure.

REFERENCES

• Bu 65: B. Buchberger: Ein AIgorithmus zum Auffinden der Basiselemente des RestklassenrirLgea nach einem nulldimenJior~alen Polyr~omideal. Dissertation, Univ. Innsbruck, Austria (1965).
• Bu 85a: B. Buchberger' "GrSbner Bases' An Algorithmic Method in Polynomial Ideal Theory". In' Multidimensional Systems Theory, N.K. Bose (ed.), 184-232, D. Reidel Publ. Comp. (1985).
• Bu 85b: Bruno Buchberger, Basic features and development of the critical-pair/completion procedure, Proc. of the first international conference on Rewriting techniques and applications, p.1-45, December 1985, Dijon, France
• BL 83: B. Buchberger, R. Loos' "Algebraic Simplification", in: Computer Algebra -- Symbolic and Algebraic Computation, 2nd ed., Buchberger, Collins, Loos (eds.), Springer-Verlag, 11-44 (1983).
• Hu 80: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• HO 80: G.P. Huet, D.C. Oppen' "Equations and Rewrite Rules ~ A Survey", in' Formal Language Theory, R.V. Book (ed.), Academic Press, 349-405 (1980).
• KK 83: A. Kandri-Rody, D. Kapur' "On Relationship between Buchberger's Grobner Basis Algorithm and the Knuth-Bendix Completion Procedure", General Electric Technical Report No. 83CRD286, Schenectady, New York (1983).
• KB 67: D.E. Knuth, P.B. Bendix' "Simple Word Problems in Universal Algebra", Proc. of the Conf. oTz Computational Problems in Abstract Algebra, Oxford, 1967, J. Leech (ed.), Pergamon Press (1970).
• Le 86: P. Le Chenandec' Canonical Forms ir~ Finitely Presented Algebras, Pitman, London (1986).
• Ll 83: R. Llopis de Trias' "Canonical Forms for Residue Classes of Polynomial Ideals and Term Rewriting Systems", Techn. Rep., Univ. Autonoma de Madrid, Division de Matematicas (1983).
• Lo 81: Rüdiger Loos, Term Reduction Systems and Algebraic Algorithms, Proceedings of the German Workshop on Artificial Intelligence, p.214-234, January 26-31, 1981
• PS 81: Gerald E. Peterson , Mark E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM (JACM), v.28 n.2, p.233-264, April 1981 [doi>10.1145/322248.322251]
• Ra 79: P. Raulefs , J. Siekmann , P. Szabó , E. Unvericht, A short survey on the state of the art in matching and unification problems, ACM SIGSAM Bulletin, v.13 n.2, p.14-20, May 1979 [doi>10.1145/1089208.1089210]
• Wi 84: F. Winkler' The Church-Ro~er Property in Compuler Algebra and Special Theorem Proving' An Investigation of Critical-Pair/Completio~ Algorithms. Dissertation, Univ. Linz (1984).

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Algebraic algorithms

General Terms:
Algorithms, Theory