Term Rewriting Systems and Algebra

  • Pierre Lescanne
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


This paper presents two ideas for proving theorems in algebra. First the equivalence of two presentations of algebras is verified by attempting to make them equivalent to the same noetherian and confluent set of rewrite rules. Second the knuth-Bendix procedures that performs that conevergence often fails by generating too big or non directable rules. We propose to tame it by an iterative approach.


Completion Procedure Directable Rule Term Rewrite System Light Symbol Computer Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    BUTLER G., LANKFORD D., “Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras” Louisiana Tech U. Math Dept. Ruston LA 71272 Dept MTP-7 Aug. 1980.Google Scholar
  2. [2]
    DERSHOWITZ N., MARCUS L., “Existence and Construction of Rewrite Systems,” Memo, Information Sciences Researsh Office, The Aerospace Corporation, El Segundo California USA, (August 1982).zbMATHGoogle Scholar
  3. [3]
    FORGAARD R., “A Program for Genersting and Analizing Term Rewriting Systems” Master’s Thesis, MIT Lab. for Comnuter Science, Cambridge Massackasetts USA (1994) (To appear)Google Scholar
  4. [4]
    HIGMAN G., NEWMAN B. H., “Groups as groupoids with one law,” Publ. Math. Debrecen. 2 (1952), 215–221.MathSciNetGoogle Scholar
  5. [5]
    HUET G., “A Complete Proof of Correctness of Knuth-Bendix Completion Algorithm,” J. Comp. Sys. Sc., 23 (1981), 11–21.MathSciNetCrossRefzbMATHGoogle Scholar
  6. [6]
    JEANROND H. J., “Deciding unique termination of permutative rewriting systems: Choose your term algebra carefully” 5th Conf. on Automated Deduction, Lectmre Notes in Computer Science 87 (1980), 335–355.Google Scholar
  7. [7]
    JOUANNAUD J-P., LESCANNE P., REINIG F., “Recursive Decomposition Ordering,” Conf. on Formal Description of Programming Concepts II, North-Holland (D Bjorner Ed.) (1982), 331–346.Google Scholar
  8. [8]
    KIRCHNER II., “Current Implementation of the general completion algorithm” Private Communication.Google Scholar
  9. [9]
    KNUTH D.E., BENDIX P.B., “Simple Word Problems in Universal Algebras,” in Computational Problems in Abstarct Algebra, Ed. Leech J., Pergamon Press (1969), 263–297.Google Scholar
  10. [10]
    LESCANNE P., “Computer Experiments with the REVE Term Rerwiting System Generator” 10th POPL Conf. Austin Texas (1983).Google Scholar
  11. [11]
    LESCANNE P., “Uniform Termination of Term Rewriting Systems: Recursive Decomposition Ordering with Status” 9th Coll. on Trees in Algebra and Programming (Bordeaux March 1984).Google Scholar
  12. [12]
    METIVIER B., “About the rewriting systems produced by the Knuth-Bendix Completion Algorithm,” Inf. Proc. Ltrs 16 (1983), 31–34.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Pierre Lescanne
    • 1
  1. 1.CRINVandoeuvre-les-NancyFrance

Personalised recommendations