Abstract
The notion of S-normalized rewriting and S-normalized completion algorithm, whose completeness has been proved for an arbitrary S, allows us to unify in a single way a variety of completion-like algorithm, as shown on figure 10.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
W. Ackermann. Solvable Cases of the Decision Problem. North-Holland, Amsterdam, 1954.
Leo Bachmair. Proof Methods for Equational Theories. PhD thesis, University of Illinois at Urbana-Champaign, 1987.
Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67 (2&3):173–201, October 1989.
W. Boone. The word problem. Annals of Math., 70:207–265, 1959.
Bruno Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Ideal. PhD thesis, University of Innsbruck, Austria, 1965. (in German).
Catherine Delor and Laurence Puel. Extension of the associative path ordering to a chain of associative-commutative symbols. In Proc. 5th Rewriting Techniques and Applications, Montréal, LNCS 690, 1993.
Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.
V. A. Emiličev. On algorithmic decidability of certain mass problems in the theory of commutative semigroups. Sbirsk. Mat. Ž, 4:788–798, 1963. In russian.
Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 2(3):326–336, September 1952.
Jean-Pierre Jouannaud and Claude Marché. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104:29–51, 1992.
Abdelilah Kandri-Rody and Deepak Kapur. An algorithm for computing the Gröbner basis of a polynomial ideal over an Euclidean ring. Technical Report 84CRD045, CRD, General Electric Company, Schenectady, New-York, December 1984.
Abdelilah Kandri-Rody and Deepak Kapur. Algorithms for computing gröbner bases of polynomial ideals over various Euclidian rings. In Proc. Eurosam 84, Cambridge, England. Springer-Verlag, 1984.
Abdelilah Kandri-Rody and Deepak Kapur. Computing the grobner basis of an ideal in polynomial rings over the integers. In V.E. Golden and M.A. Hussain, editors, Proc. of the Thirds MACSYMA Users'Conference, July 1984.
Abdelilah Kandri-Rody, Deepak Kapur, and Franz Winkler. Knuth-Bendix procedure and Buchberger algorithm — a synthesis. In Proc. of the 20th Int. Symp. on Symbolic and Algebraic Computation, Portland, Oregon, pages 55–67, 1989.
Deepak Kapur and Paliath Narendran. Constructing Gröbner bases for a polynomial ideal. Presented at the workshop Combinatorial algorithms in algebraic structures at Europaische Akademie, Otzenhause, 1985.
Claude Kirchner, editor. Unification. Academic Press, 1990.
Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, 1970.
Dallas S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Research Report Memo ATP-39, Department of Mathematics and Computer Science, University of Texas, Austin, Texas, USA, August 1977.
Philippe Le Chenadec. Canonical forms in finitely presented algebras. Pitman, London, 1986.
Claude Marché. The word problem of ACD-ground theories is undecidable. International Journal of Foundations of Computer Science, 3(1):81–92, 1992.
Claude Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certains classes de théories équationnelles. Thèse de Doctorat, Université de Paris-Sud, France, 1993.
A. A. Markov. On the impossibility of certain algorithms in the theory of associative systems. Dokl. Akad. Nauk SSSR, 55(7):587–590, 1947. In Russian, English translation in C.R. Acad. Sci. URSS, 55, 533–586.
Paliath Narendran and Michaël Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In Ronald V. Book, editor, Proc. 4th Rewriting Techniques and Applications, LNCS 488, Como, Italy, April 1991. Springer-Verlag.
P. S. Novikov. On the algorithmic unsolvability of the word problem in group theory. Trudy Mat. Inst. Steklov, 44:1–143, 1955. in Russian.
Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233–264, April 1981.
Emil L. Post. Recursive unsolvability of a problem of Thue. Journal of Symbolic Logic, 13:1–11, 1947.
D. A. Smith. A basis algorithm for finitely generated Abelian groups. Maths. Algorithms, I(1), 1966.
John Stillwell. The word problem and the isomorphism problem for groups. Bulletin of the American Mathematical Society, 6(1):33–56, January 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marché, C. (1995). Normalized rewriting — Application to ground completion and standard bases. In: Comon, H., Jounnaud, JP. (eds) Term Rewriting. TCS School 1993. Lecture Notes in Computer Science, vol 909. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59340-3_12
Download citation
DOI: https://doi.org/10.1007/3-540-59340-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59340-9
Online ISBN: 978-3-540-49237-5
eBook Packages: Springer Book Archive