Term Rewriting Systems and Algebra
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.
KeywordsCompletion Procedure Directable Rule Term Rewrite System Light Symbol Computer Proof
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- KIRCHNER II., “Current Implementation of the general completion algorithm” Private Communication.Google Scholar
- 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
- LESCANNE P., “Computer Experiments with the REVE Term Rerwiting System Generator” 10th POPL Conf. Austin Texas (1983).Google Scholar
- 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