{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:36:24Z","timestamp":1725456984499},"publisher-location":"Berlin\/Heidelberg","reference-count":55,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540528261"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0032044","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:05:31Z","timestamp":1134281131000},"page":"350-369","source":"Crossref","is-referenced-by-count":9,"title":["Term rewriting systems from Church-Rosser to Knuth-Bendix and beyond"],"prefix":"10.1007","author":[{"given":"Jan Willem","family":"Klop","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"BACHMAIR, L. (1988). Proof by consistency in equational theories. In: Proc. 3rd Symp. on Logic in Computer Science, Edinburgh. 228\u2013233.","DOI":"10.1109\/LICS.1988.5122"},{"key":"28_CR2","unstructured":"BACHMAIR, L., DERSHOWITZ, N. & HSIANG, J. (1986). Orderings for equational proofs. In: Proc. of the IEEE Symp. on Logic in Computer Science, Cambridge, Massachusetts, 346\u2013357."},{"key":"28_CR3","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1016\/0304-3975(89)90006-6","volume":"67","author":"J.C.M. Baeten","year":"1988","unstructured":"BAETEN, J.C.M., BERGSTRA, J.A., KLOP, J.W. & W.P. Weijland. (1988). Term rewriting systems with rule priorities. TCS 67 (1989) 283\u2013301.","journal-title":"TCS"},{"key":"28_CR4","unstructured":"BARENDREGT, H.P. (1984). The Lambda Calculus, its Syntax and Semantics. 2nd ed. North-Holland 1984."},{"key":"28_CR5","volume-title":"Handbook of Theoretical Computer Science","author":"H.P. Barendregt","year":"1989","unstructured":"BARENDREGT, H.P. (1989). Functional programming and lambda calculus. In: Handbook of Theoretical Computer Science (ed. J. van Leeuwen), North-Holland, Amsterdam."},{"key":"28_CR6","first-page":"141","volume":"259","author":"H.P. Barendregt","year":"1987","unstructured":"BARENDREGT, H.P., VAN EEKELEN, M.C.J.D., GLAUERT, J.R.W., KENNAWAY, J.R., PLASMEIJER, M.J. & SLEEP, M.R. (1987). Term graph rewriting. In: Proc. PARLE Conf., Springer LNCS 259, 141\u2013158.","journal-title":"Springer LNCS"},{"issue":"3","key":"28_CR7","first-page":"323","volume":"32","author":"J.A. Bergstra","year":"1986","unstructured":"BERGSTRA, J.A. & KLOP, J.W. (1986). Conditional rewrite rules: confluence and termination. JCSS 32 (3), 323\u2013362.","journal-title":"JCSS"},{"key":"28_CR8","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","volume":"31","author":"G. Birkhoff","year":"1935","unstructured":"BIRKHOFF, G. (1935). On the structure of abstract algebras. In: Proc. of the Cambridge Philosophical Society 31, 433\u2013454.","journal-title":"Proc. of the Cambridge Philosophical Society"},{"key":"28_CR9","unstructured":"DE BRUIJN, N.G. (1978). A note on weak diamond properties. Memorandum 78-08, Eindhoven Univ. of Technology, 1978."},{"key":"28_CR10","series-title":"Research Notes in Theoretical Computer Science","volume-title":"Categorical combinators, sequential algorithms and functional programming","author":"P.-L. Curien","year":"1986","unstructured":"CURIEN, P.-L. (1986). Categorical combinators, sequential algorithms and functional programming. Research Notes in Theoretical Computer Science, Pitman, London 1986."},{"key":"28_CR11","unstructured":"DAUCHET, M., TISON, S., HEUILLARD, T. & LESCANNE, P. (1987). Decidability of the confluence of ground term rewriting systems. In: Proc. of the 2nd Symp. on Logic in Computer Science, Ithaca, NY, 1987, 353\u2013359."},{"issue":"1&2","key":"28_CR12","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"DERSHOWITZ, N. (1987). Terminationof rewriting. J. of Symbolic Computation 3 (1&2), 69\u2013115, 1987. Corrigendum: Vol.4, No.3, 409\u2013410.","journal-title":"J. of Symbolic Computation"},{"key":"28_CR13","unstructured":"DERSHOWITZ, N. & JOUANNAUD, J.-P. (1989). Rewrite systems. To appear as Chapter 15 of Vol.B of \u201cHandbook of Theoretical Computer Science\u201d, North-Holland, 1989. (Rapport de R\u00e9cherche no.478, Unit\u00e9 Associ\u00e9e au CNRS UA 410: AL KHOWARIZMI, Avril 1989.)"},{"key":"28_CR14","first-page":"31","volume":"308","author":"N. Dershowitz","year":"1987","unstructured":"DERSHOWITZ, N., OKADA, M. & SIVAKUMAR, G. (1987). Confluence of Conditional Rewrite Systems. In: Proc. of the 1st International Workshop on Conditional Term Rewrite Systems, Orsay, Springer LNCS 308, 31\u201344.","journal-title":"Springer LNCS"},{"key":"28_CR15","first-page":"538","volume":"310","author":"N. Dershowitz","year":"1988","unstructured":"DERSHOWITZ, N., OKADA, M. & SIVAKUMAR, G. (1988). Canonical Conditional Rewrite Systems. In: Proc. of 9th Conf. on Automated Deduction, Argonne, Springer LNCS 310, 538\u2013549.","journal-title":"Springer LNCS"},{"key":"28_CR16","unstructured":"DERSHOWITZ, N. & PLAISTED, D.A. (1987). Equational Programming. In: Machine Intelligence 11 (eds. J.E. Hayes, D. Michie and J. Richards), Oxford University Press, 21\u201356."},{"key":"28_CR17","first-page":"62","volume":"308","author":"H. Ganzinger","year":"1987","unstructured":"GANZINGER, H. (1987). A completion procedure for conditional equations. In: Proc of the 1st Intern. Workshop on Conditional Term Rewriting Systems, Orsay 1987, Springer LNCS 308, 1988, 62\u201383.","journal-title":"Springer LNCS"},{"key":"28_CR18","unstructured":"GOGUEN, J.A. & MESEGUER, J. (1985). Initiality, induction, and computability. In: Algebraic methods in semantics (eds. M. Nivat and J.C. Reynolds), Cambridge University Press 1985, 459\u2013542."},{"issue":"3","key":"28_CR19","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","volume":"65","author":"T. Hardin","year":"1989","unstructured":"HARDIN, T. (1989). Confluence results for the pure Strong Categorical Logic CCL. \u03bb-calculi as subsystems of CCL. Theor. Comput Sci. Fundamental Studies, Vol.65, Nr.3, 1989, 291\u2013342.","journal-title":"Theor. Comput Sci. Fundamental Studies"},{"key":"28_CR20","unstructured":"HINDLEY, J.R. & SELDIN, J.P. (1986). Introduction to Combinators and \u03bb-Calculus. London Mathematical Society Student Texts, Nr.1, Cambridge University Press 1986."},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"H\u00d6LLDOBLER, S. (1989). Foundations of Equational Logic Programming. Springer Lecture Notes in A.I. 353.","DOI":"10.1007\/BFb0015791"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"HSIANG, J. (1985). Refutational Theorem Proving using Term-Rewriting Systems. Artificial Intelligence, 25, Vol.3, 1985.","DOI":"10.1016\/0004-3702(85)90074-8"},{"issue":"4","key":"28_CR23","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"HUET, G. (1980). Confluent reductions: Abstract properties and applications to term rewriting systems. JACM, Vol.27, No.4 (1980), 797\u2013821.","journal-title":"JACM"},{"key":"28_CR24","unstructured":"HUET, G. & LANKFORD, D.S. (1978). On the uniform halting problem for term rewriting systems. Rep. 283, IRIA."},{"key":"28_CR25","unstructured":"HUET, G. & L\u00c9VY, J.-J. (1979). Call-by-need computations in non-ambiguous linear term rewriting systems. Rapport INRIA nr.359."},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"HUET, G. & OPPEN, D.C. (1980). Equations and rewrite rules: A survey. In: Formal Language Theory: Perspectives and Open Problems (ed. R. Book), Academic Press, 1980, 349\u2013405.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"KAPLAN, S. (1984). Conditional Rewrite Rules. TCS 33(2,3), 1984.","DOI":"10.1016\/0304-3975(84)90087-2"},{"key":"28_CR28","volume-title":"Recent Trends in Data Type Specification","author":"S. Kaplan","year":"1985","unstructured":"KAPLAN, S. (1985). Fair conditional term rewriting systems: Unification, termination and confluence, Recent Trends in Data Type Specification (ed. H.-J. Kreowski), Informatik-Fachberichte 116, Springer-Verlag, Berlin, 1985."},{"key":"28_CR29","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0168-0072(89)90024-9","volume":"43","author":"J.R. Kennaway","year":"1989","unstructured":"KENNAWAY, J.R. (1989). Sequential evaluation strategies for parallel-or and related reduction systems. Annals of Pure and Applied Logic 43 (1989) 31\u201356.","journal-title":"Annals of Pure and Applied Logic"},{"key":"28_CR30","unstructured":"KLOP, J.W. (1980). Combinatory Reduction Systems. Mathematical Centre Tracts Nr.127, CWI, Amsterdam."},{"key":"28_CR31","unstructured":"KLOP, J.W. (1990). Term Rewriting Systems, in: Handbook of Logic in Computer Science (eds. S. Abramsky, D. Gabbay and T. Maibaum) Vol.1, Chapter 6, Oxford University Press, to appear."},{"issue":"2","key":"28_CR32","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0890-5401(89)90014-X","volume":"80","author":"J.W. Klop","year":"1989","unstructured":"KLOP, J.W. & DE VRIJER, R.C. (1989). Unique Normal Forms for Lambda Calculus with Surjective Pairing. Information and Computation 80 (2), 97\u2013113.","journal-title":"Information and Computation"},{"key":"28_CR33","unstructured":"KNUTH, D.E. & BENDIX, P.B. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra (ed. J. Leech), Pergamon Press, 1970, 263\u2013297."},{"key":"28_CR34","first-page":"210","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"KRUSKAL, J.B. (1960). Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture. Trans. AMS 95, 210\u2013225.","journal-title":"Trans. AMS"},{"key":"28_CR35","unstructured":"KURIHARA, M. & KAJI, I. (1988). Modular Term Rewriting Systems: Termination, Confluence and Strategies. Report, Hokkaido University."},{"key":"28_CR36","volume-title":"Modularity of Simple Termination of Term Rewriting Systems. Report 89-SF-31","author":"M. Kurihara","year":"1989","unstructured":"KURIHARA, M. & OHUCHI, A. (1989) Modularity of Simple Termination of Term Rewriting Systems. Report 89-SF-31, Hokkaido University, Sapporo, 1989."},{"key":"28_CR37","first-page":"263","volume":"355","author":"A. Middeldorp","year":"1989","unstructured":"MIDDELDORP, A. (1989a). Modular aspects of properties of term rewriting systems related to normal forms. In: Proc. of 3rd Intern. Conf. on Rewriting Techniques and Applications, Chapel Hill, Springer LNCS 355, 263\u2013277.","journal-title":"Springer LNCS"},{"key":"28_CR38","doi-asserted-by":"crossref","unstructured":"MIDDELDORP, A. (1989b). A sufficient condition for the termination of the direct sum of term rewriting systems. In: Proc. of 4th IEEE Symposium on Logic in Computer Science, Pacific Grove, 396\u2013401.","DOI":"10.1109\/LICS.1989.39194"},{"key":"28_CR39","volume-title":"Confluence of the Disjoint Union of Conditional Term Rewriting Systems. Report CS-R8944","author":"A. Middeldorp","year":"1989","unstructured":"MIDDELDORP, A. (1989c). Confluence of the Disjoint Union of Conditional Term Rewriting Systems. Report CS-R8944, Centre for Mathematics and Computer Science, Amsterdam 1989."},{"issue":"2","key":"28_CR40","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. (1942). On theories with a combinatorial definition of \u201cequivalence\u201d. Annals of Math. 43 (2), 223\u2013243.","journal-title":"Annals of Math."},{"key":"28_CR41","doi-asserted-by":"crossref","unstructured":"O'DONNELL, M.J. (1977). Computing in systems described by equations. Springer LNCS 58.","DOI":"10.1007\/3-540-08531-9"},{"key":"28_CR42","volume-title":"Equational logic as a programming language","author":"M.J. O'Donnell","year":"1985","unstructured":"O'DONNELL, M.J. (1985). Equational logic as a programming language. The MIT Press, Cambridge MA, 1985."},{"key":"28_CR43","doi-asserted-by":"crossref","unstructured":"OYAMAGUCHI, M. (1987). The Church-Rosser property for ground term rewriting systems is decidable. Theoretical Computer Science 49 (1).","DOI":"10.1016\/0304-3975(87)90100-9"},{"key":"28_CR44","unstructured":"PEYTON JONES, S.L. (1987). The Implementation of Functional Programming Languages. Prentice-Hall 1987."},{"key":"28_CR45","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"B.K. Rosen","year":"1973","unstructured":"ROSEN, B.K. (1973). Tree-manipulating systems and Church-Rosser theorems. JACM, Vol.20 (1973), 160\u2013187.","journal-title":"JACM"},{"key":"28_CR46","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(87)90039-1","volume":"26","author":"M. Rusinowitch","year":"1987","unstructured":"RUSINOWITCH, M. (1987). On termination of the direct sum of term rewriting systems IPL 26, 65\u201370.","journal-title":"IPL"},{"key":"28_CR47","unstructured":"SCH\u00d6NFINKEL, M. (1924). \u00dcber die Bausteine der mathematischen Logik. Math. Annalen 92, 305\u2013316. Translated as: On the building blocks of mathematical logic, in From Frege to G\u00f6del, ed. J. van Heyenoort, Harvard Un. Press, 1967, 355\u2013366."},{"key":"28_CR48","first-page":"346","volume":"37","author":"D.S. Scott","year":"1975","unstructured":"SCOTT, D.S. (1975). Some philosophical issues concerning theories of combinators. In: Proc. of Symposium \u2018\u03bb-calculus and Computer Science Theory', (ed. C. B\u00f6hm), Rome 1975, Springer LNCS 37, 346\u2013366.","journal-title":"Springer LNCS"},{"key":"28_CR49","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BFb0062861","volume":"450","author":"J. Staples","year":"1975","unstructured":"STAPLES, J. (1975). Church-Rosser theorems for replacement systems. In: Algebra and Logic (ed. J. Crosley), Springer Lecture Notes in Mathematics 450, 291\u2013307.","journal-title":"Springer Lecture Notes in Mathematics"},{"key":"28_CR50","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"TOYAMA, Y. (1987a). Counterexamples to termination for the direct sum of Term Rewriting Systems. Information Processing Letters 25, 141\u2013143.","journal-title":"Information Processing Letters"},{"issue":"1","key":"28_CR51","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"TOYAMA, Y. (1987b). On the Church-Rosser property for the direct sum of term rewriting systems. JACM, Vol.34, No.1, 1987, 128\u2013143.","journal-title":"JACM"},{"key":"28_CR52","first-page":"477","volume":"355","author":"Y. Toyama","year":"1989","unstructured":"TOYAMA, Y., KLOP, J.W. & BARENDREGT, H.P. (1989). Termination for the direct sum of left-linear term rewriting systems. In: Proc. of 3rd Intern. Conf. on Rewriting Techniques and Applications, Springer LNCS 355, 477\u2013491.","journal-title":"Springer LNCS"},{"key":"28_CR53","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1002\/spe.4380090105","volume":"9","author":"D.A. Turner","year":"1979","unstructured":"TURNER, D.A. (1979). A new implementation technique for applicative languages. Software Practice and Experience, Vol.9, 1979, 31\u201349.","journal-title":"Software Practice and Experience"},{"key":"28_CR54","doi-asserted-by":"crossref","unstructured":"TURNER, D.A., (1985). Miranda: a non-strict functional language with polymorphic types. In: Proc. of the IFIP Intern. Conf. on Functional Programming Languages and Computer Architecture, Nancy. Springer LNCS 201, 1985.","DOI":"10.1007\/3-540-15975-4_26"},{"key":"28_CR55","doi-asserted-by":"crossref","unstructured":"WINKLER, F. & BUCHBERGER, B. (1983). A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Proc. of the Coll. on Algebra, Combinatorics and Logic in Computer Science, Gy\u00f6r, Hungary, Sept. 1983.","DOI":"10.1145\/1089338.1089341"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0032044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:44:43Z","timestamp":1586612683000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0032044"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540528261"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/bfb0032044","relation":{},"subject":[]}}