{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:15:26Z","timestamp":1725664526336},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593409"},{"type":"electronic","value":"9783540492375"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59340-3_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:14:24Z","timestamp":1330258464000},"page":"1-15","source":"Crossref","is-referenced-by-count":2,"title":["Introduction to rewriting"],"prefix":"10.1007","author":[{"given":"Jean-Pierre","family":"Jouannaud","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"1","key":"1_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"Leo Bachmair and Nachum Dershowitz. Critical pair criteria for completion. Journal of Symbolic Computation, 6(1):1\u201318, 1988.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder. Basic paramodulation and superposition. In Deepak Kapur, editor, Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNCS 607. Springer-Verlag, June 1992.","DOI":"10.1007\/3-540-55602-8_185"},{"issue":"4","key":"1_CR3","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1142\/S0129054190000278","volume":"1","author":"H. Comon","year":"1990","unstructured":"Hubert Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387\u2013411, 1990.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Max Dauchet. Simulation of a turing machine by a left-linear rewrite rule. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, 1989.","DOI":"10.1007\/3-540-51081-8_103"},{"key":"1_CR5","unstructured":"Nachum Dershowitz. Applications of the Knuth-Bendix completion procedure. In Proceedings of the Seminaire d'Informatique Th\u00e9orique, pages 95\u2013111, Paris, France, December 1982."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Charles Hoot. Topics in termination. In Proc. 5th Rewriting Techniques and Applications, Montr\u00e9al, LNCS 690, 1993.","DOI":"10.1007\/3-540-56868-9_16"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243\u2013309. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"1_CR8","volume-title":"Th\u00e8se de Doctorat","author":"H. Devie","year":"1991","unstructured":"Herv\u00e9 Devie. Une approche alg\u00e9brique de la r\u00e9\u00e9criture de preuves \u00e9quationnelles et son application \u00e0 la d\u00e9rivation de proc\u00e9dures de compl\u00e9tion. Th\u00e8se de Doctorat, Universit\u00e9 de Paris-Sud, France, Octobre 1991."},{"key":"1_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01189020","volume":"3","author":"M. Fern\u00e1ndez","year":"1992","unstructured":"Maribel Fern\u00e1ndez. Narrowing based procedures for equational disunification. Applicable Algebra in Engineering Communication and Computing, 3:1\u201326, 1992.","journal-title":"Applicable Algebra in Engineering Communication and Computing"},{"key":"1_CR10","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"Laurent Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253\u2013276, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and Jose Meseguer. Principles of OBJ2. In Proc. 12th ACM Symp. Principles of Programming Languages, New Orleans, 1985.","DOI":"10.1145\/318593.318610"},{"issue":"4","key":"1_CR12","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G\u00e9rard Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797\u2013821, October 1980.","journal-title":"Journal of the ACM"},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G\u00e9rard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. Journal of Computer and System Sciences, 23:11\u201321, 1981.","journal-title":"Journal of Computer and System Sciences"},{"key":"1_CR14","unstructured":"G\u00e9rard Huet and Dallas S. Lankford. On the uniform halting problem for term rewriting systems. Research Report 283, INRIA, March 1978."},{"key":"1_CR15","unstructured":"G\u00e9rard Huet and Jean-Jacques L\u00e9vy. Computations in orthogonal term rewriting systems. In Gordon Plotkin and Jean-Louis Lassez, editors, Computational Logic: essays in Honour of Alan Robinson. MIT Press, 1990."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1), July 1989.","DOI":"10.1016\/0890-5401(89)90062-X"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordinal notations with the subterm property is decidable. In Proc. 18th Int. Coll. on Automata, Languages and Programming, Madrid, LNCS 510, 1991.","DOI":"10.1007\/3-540-54233-7_155"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"H\u00e9l\u00e8ne Kirchner and M. Hermann. Metarule inference from crossed rewrite systems. Draft version, presented at CTRS, Montreal, 1990.","DOI":"10.1007\/3-540-54317-1_87"},{"key":"1_CR19","unstructured":"Jan Willem Klop. Term Rewriting Systems. In S. Abramsky, Dov.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 1\u2013116. Clarendon Press, 1992."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"1_CR21","volume-title":"Th\u00e8se de Doctorat","author":"C. March\u00e9","year":"1993","unstructured":"Claude March\u00e9. R\u00e9\u00e9criture modulo une th\u00e9orie pr\u00e9sent\u00e9e par un syst\u00e8me convergent et d\u00e9cidabilit\u00e9 des probl\u00e8mes du mot dans certains classes de th\u00e9ories \u00e9quationnelles. Th\u00e8se de Doctorat, Universit\u00e9 de Paris-Sud, France, 1993."},{"issue":"1","key":"1_CR22","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0020-0190(83)90009-1","volume":"16","author":"Y. M\u00e9tivier","year":"1983","unstructured":"Y. M\u00e9tivier. About the rewriting systems produced by the knuth-bendix completion algorithm. Information Processing Letters, 16(1):31\u201334, 1983.","journal-title":"Information Processing Letters"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"D. Musser. Proving inductive properties of abstract data types. In Proc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, 1980.","DOI":"10.1145\/567446.567461"},{"issue":"2","key":"1_CR24","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. H. A. Newman","year":"1942","unstructured":"M. H. A. Newman. On theories with a combinatorial definition of \u2018equivalence'. Ann. Math., 43(2):223\u2013243, 1942.","journal-title":"Ann. Math."},{"key":"1_CR25","first-page":"371","volume-title":"Proc. European Symp. on Programming, LNCS 582","author":"R. Nieuwenhuis","year":"1992","unstructured":"Robert Nieuwenhuis and Albert Rubio. Basic superposition is complete. In B. Krieg-Bruckner, editor, Proc. European Symp. on Programming, LNCS 582, pages 371\u2013389, Rennes, 1992. Springer-Verlag."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"M. J. O'Donnell. Equational Logic as a Programming Language. MIT Press, 1986.","DOI":"10.1007\/3-540-15648-8_20"},{"issue":"1","key":"1_CR27","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"B. K. Rosen","year":"1973","unstructured":"Barry K. Rosen. Tree-manipulating systems and church-rosser theorems. J. of the Association for Computing Machinery, 20(1):160\u2013187, January 1973.","journal-title":"J. of the Association for Computing Machinery"},{"key":"1_CR28","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1016\/S0747-7171(08)80020-X","volume":"9","author":"H. Zhang","year":"1990","unstructured":"H. Zhang. Automated proof of ring commutativity problems by algebraic methods. Journal of Symbolic Computation, 9:423\u2013427, 1990.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59340-3_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:26:55Z","timestamp":1605630415000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59340-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593409","9783540492375"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-59340-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}