Fast Knuth-Bendix completion: Summary

  • Jim Christian
System Descriptions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    J-P. Jouannaud, H. Kirchner. (1984) Completion of a Set of Rules Modulo a Set of Equations. Proceedings 11th POPL, Salt Lake City.Google Scholar
  2. [2]
    C. Kirchner. (1987) Methods and Tools for Equational Unification. Proceedings of the Colloquium on the Resolution of Equations in Algebraic Structures, Lakeway, Texas.Google Scholar
  3. [3]
    D. Knuth and P. Bendix. (1970) Simple Word Problems in Universal Algebras. in J. Leech, ed., Computational Problems in Abstract Algebra, 263–297, Pergamon Press, Oxford, U.K.Google Scholar
  4. [4]
    D. Lankford, M. Ballantyne. (1977) Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. U.T. Austin Math Tech Report ATP-35.Google Scholar
  5. [5]
    P. Lincoln and J. Christian. (1988) Adventures in Associative-Commutative Unification. Proceedings CADE-9 358–367. Full version to appear in Journal of Symbolic Computation.Google Scholar
  6. [6]
    R. Lusk, W. McCune, R. Overbeek. Implementation of Theorem Provers: An Argonne Perspective. Lecture notes from a seminar at CADE-9.Google Scholar
  7. [7]
    G. Peterson, M. Stickel. (1981) Complete Sets of Reductions for Some Equational Theories. JACM 28, 233–264.Google Scholar
  8. [8]
    D. H. Warren. (1983) An Abstract Prolog Instruction Set. SRI Technical Note 309.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Jim Christian
    • 1
  1. 1.Dept. of Computer SciencesThe University of Texas at AustinAustin

Personalised recommendations