{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:31Z","timestamp":1725663151149},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540502418"},{"type":"electronic","value":"9783540459606"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50241-6_41","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:18:24Z","timestamp":1330201104000},"page":"235-262","source":"Crossref","is-referenced-by-count":2,"title":["A survey of rewrite systems"],"prefix":"10.1007","author":[{"given":"P. H.","family":"Schmitt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"17_CR1","unstructured":"Avenhaus, J\u00fcrgen, On the Termination of the Knuth-Bendix Completion Algorithm Technical Report 120\/84, Universit\u00e4t Kaiserslautern, Fachbereich Informatik, 1984."},{"key":"17_CR2","unstructured":"The Lambda Calculus, Studies in Logic, Vol. 103, North-Holland Publ. Co. 1984."},{"key":"17_CR3","unstructured":"Bauer, G. Zur Darstellung von Monoiden durch konfluente Regelsysteme. Dissertation, Universit\u00e4t Kaiserslautern, Fachbereich Informatik, 1981."},{"key":"17_CR4","volume-title":"Homological Dimension of Discrete Groups","author":"R. Bieri","year":"1976","unstructured":"Bieri, R. Homological Dimension of Discrete Groups Queen Mary College Mathematics Notes, London, 1976."},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/S0747-7171(87)80021-4","volume":"1","author":"R.V. Book","year":"1987","unstructured":"Book, R.V. Thue Systems as Rewriting Systems J. of Symbolic Computation, Vol. 1 & 2, 1987, pp.39\u201368.","journal-title":"J. of Symbolic Computation"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Bose, N.K. (ed.) Recent Trends in Multidimensional systems Theory Reidel Publ. Co., 1985","DOI":"10.1007\/978-94-009-5225-6"},{"key":"17_CR7","unstructured":"Book, Ronald, V. Formal Language Theory, Academic Press, 1980."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Buchberger, B., Loos, R. Algebraic Simplification, in (Buchberger et al. 1982) pp. 11\u201343.","DOI":"10.1007\/978-3-7091-3406-1_2"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Buchberger, B., Collins, G. Loos, R. (eds.), Computer Algebra \u2014 Symbolic and Algebraic Computation, Springer Verlag, 1982.","DOI":"10.1007\/978-3-7091-3406-1"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Buchberger, B. Gr\u00f6bner Bases: An Algorithmic Method in Polynomial Ideal Theory in (Bose 1985) pp.","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"17_CR11","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","volume":"3","author":"B. Buchberger","year":"1987","unstructured":"Buchberger, Bruno History and Basic Features of the Critical-Pair\/Completion Procedure J. Symbolic Computation, vol. 3, 1987, pp. 3\u201338","journal-title":"J. Symbolic Computation"},{"key":"17_CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, Nachum. Orderings for Term-Rewriting Systems, Theoretical Computer Science, vol. 17, 1982, pp. 279\u2013301.","journal-title":"Theoretical Computer Science"},{"key":"17_CR13","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, Nachum. Termination of Rewriting J. Symbolic Computation, vol. 3, 1987, pp. 69\u2013116. (revised version of the contribution in (Jouannaud 1985))","journal-title":"J. Symbolic Computation"},{"key":"17_CR14","unstructured":"Dietrich, Roland. Eine Programmierumgebung f\u00fcr Termersetzungssysteme, Arbeitspapiere der GMD, Nr. 130, Gesellschaft f\u00fcr Mathematik und Datenverarbeitung mbH, Schlo\u00df Birlinghofen, Postfach 1240, 5205 Sankt Augustin 1."},{"key":"17_CR15","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1002\/malq.19710170117","volume":"17","author":"G. Herman","year":"1971","unstructured":"Herman, G. Strong computability and variants of the uniform halting problem Zeitschrift f. Math. Logik Grundl. Math. vol. 17, 1971, pp. 115\u2013131.","journal-title":"Zeitschrift f. Math. Logik Grundl. Math."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Huet, G\u00e9rard, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, 18 th. IEEE Symposium on Foundations of Compoter Science, 1977, pp. 30\u201345.","DOI":"10.1109\/SFCS.1977.9"},{"key":"17_CR17","unstructured":"Huet, G\u00e9rard and Lankford, Dallas, On the Uniform Halting Problem for Term Rewriting Systems Rapport de Recherche No 283, 1978, IRIA (Institute de Recherche d'Informatique et d'Automatique), Rocquencourt, BP 105 78150 Le Chesnay, France."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Huet, G\u00e9rard and Oppen, Derek, C. Equations and Rewrite Rules, in (Book 1980), pp. 349\u2013405.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"17_CR19","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"Huet, G\u00e9rard, A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm J. of Computer and Systems Science, vol. 23, 1981, pp. 11\u201321.","journal-title":"J. of Computer and Systems Science"},{"key":"17_CR20","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0020-0190(85)90018-3","volume":"21","author":"M. Jouannaud","year":"1985","unstructured":"Jouannaud, M. A note on a special one-rule semi-Thue system Conference in Dijon, May 1985 Inf. Proc. Letters 21 (1985), 135\u2013140.","journal-title":"Inf. Proc. Letters"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Jouannaud, Jean-Pierre (ed.) Rewriting Techniques and Applications, Proceedings of the Conference in Dijon, May 1985 Springer Lecture Notes in Computer Science, Vol. 202, 1985","DOI":"10.1007\/3-540-15976-2"},{"key":"17_CR22","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1016\/0304-3975(85)90023-4","volume":"35","author":"D. Kapur","year":"1985","unstructured":"Kapur, D., Narendran, P. A finite Thue system with decidable word problem and without equivalent finite canonical system Theoret. Comput. Science 35 (1985) 337\u2013344.","journal-title":"Theoret. Comput. Science"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Knuth, D. E. and Bendix, P. B., Simple Word Problems in Universal algebra, in: (Leech 1967), pp. 263\u2013297.","DOI":"10.1007\/978-3-642-81955-1_23"},{"key":"17_CR24","first-page":"210","volume":"95","author":"J. B. Kruskal","year":"1960","unstructured":"Kruskal, J. B. Well-quasi-orderings, the Tree Theorem, and Vazsonyis's Conjecture Trans. Amer. Math. Soc. Vol. 95, 1960, pp. 210\u2013225.","journal-title":"Trans. Amer. Math. Soc."},{"volume-title":"Computational Problems in Abstract","year":"1967","key":"17_CR25","unstructured":"Leech, J. (ed.) Computational Problems in Abstract, Pergamon Press, Cambridge, 1967."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Lescanne, Pierre (ed.) Rewriting Techniques and Applications, Proceedings of the Conference in Bordeaux, May 1987 Springer Lecture Notes in Computer Science, Vol. 256, 1987","DOI":"10.1007\/3-540-17220-3"},{"key":"17_CR27","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","volume":"59","author":"C. S. J. Nash-Williams","year":"1963","unstructured":"Nash-Williams, C. St. J.A. On well-quasi-ordering finite trees. Proc. Cambridge Philos. Soc. vol. 59, 1963, pp. 833\u2013835.","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"17_CR28","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M.H.A. Newman","year":"1942","unstructured":"Newman, M.H.A. On Theories with a Combinatorial Definition of \u201cEquivalence\u201d, Annals of Math., vol. 43, 1942, pp. 223\u2013243.","journal-title":"Annals of Math."},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Otto, Fr. and Squier, C. The Word Problem for Finitely Presented Monoids and Finite Canonical Rewrite Systems in: (Lescanne 1987) pp. 74\u201382.","DOI":"10.1007\/3-540-17220-3_7"},{"key":"17_CR30","unstructured":"Ruckert, Martin Church-Rosser Theorem 12nd Normalisierung f\u00fcr Termkalk\u00fcle mit unendlichen Termen unter Einschlu\u00df permutativer Reduktionen Dissertation, Fakult\u00e4t f\u00fcr Mathematik, Ludwig-Maximilian-Universit\u00e4t M\u00fcnchen, 1985."}],"container-title":["Lecture Notes in Computer Science","CSL '87"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50241-6_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:45Z","timestamp":1605647865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50241-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540502418","9783540459606"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-50241-6_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}