{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:19:53Z","timestamp":1759637993256},"publisher-location":"Berlin, Heidelberg","reference-count":100,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_28","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"376-393","source":"Crossref","is-referenced-by-count":3,"title":["Open. Closed. Open."],"prefix":"10.1007","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"28_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. J. Symbolic Computation\u00a06(1), 1\u201318 (1988)","journal-title":"J. Symbolic Computation"},{"key":"28_CR2","series-title":"Rewriting Techniques","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, vol.\u00a02, ch. 1, pp. 1\u201330. Academic Press, New York (1989)"},{"key":"28_CR3","volume-title":"The Lambda Calculus, its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus, its Syntax and Semantics, 2nd edn. North-Holland, Amsterdam (1984)","edition":"2"},{"issue":"1","key":"28_CR4","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0304-3975(94)90066-3","volume":"123","author":"A. Bertrand","year":"1994","unstructured":"Bertrand, A.: Sur une conjecture d\u2019YvesM\u00e9tivier. Theoretical Computer Science\u00a0123(1), 21\u201330 (1994)","journal-title":"Theoretical Computer Science"},{"key":"28_CR5","first-page":"86","volume":"79","author":"M. Bezem","year":"2003","unstructured":"Bezem, M., Coquand, T.: Newman\u2019s Lemma \u2013 a case study in proof automation and geometric logic (Logic in Computer Science Column). Bulletin of the EATCS\u00a079, 86\u2013100 (2003)","journal-title":"Bulletin of the EATCS"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic (to appear)","DOI":"10.1145\/1182613.1182619"},{"key":"28_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9771-7","volume-title":"String-Rewriting Systems","author":"R.V. Book","year":"1993","unstructured":"Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993)"},{"key":"28_CR8","unstructured":"de Bruijn, N.G.: A note on weak diamond properties. Memorandum 1978-08, Department of Mathematics, Eindhoven University of Technology, Eindhoven, The Netherlands (August 1978)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/3-540-53982-4_5","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"A.-C. Caron","year":"1991","unstructured":"Caron, A.-C.: Linear bounded automata and rewrite systems: Influence of initial configurations on decision properties. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol.\u00a0493, pp. 74\u201389. Springer, Heidelberg (1991)"},{"key":"28_CR10","series-title":"Ann. Mathematics Studies","volume-title":"The Calculi of Lambda Conversion","author":"A. Church","year":"1941","unstructured":"Church, A.: The Calculi of Lambda Conversion. Ann. Mathematics Studies, vol.\u00a06. Princeton University Press, Princeton (1941)"},{"key":"28_CR11","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","volume":"39","author":"A. Church","year":"1936","unstructured":"Church, A., Rosser, J.B.: Some properties of conversion. Transactions of the American Mathematical Society\u00a039, 472\u2013482 (1936)","journal-title":"Transactions of the American Mathematical Society"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/3-540-51081-8_103","volume-title":"Rewriting Techniques and Applications","author":"M. Dauchet","year":"1989","unstructured":"Dauchet, M.: Simulation of Turing machines by a left-linear rewrite rule. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 109\u2013120. Springer, Heidelberg (1989)"},{"issue":"2","key":"28_CR13","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/0304-3975(92)90022-8","volume":"103","author":"M. Dauchet","year":"1992","unstructured":"Dauchet, M.: Simulation of Turing machines by a regular rewrite rule. Theoretical Computer Science\u00a0103(2), 409\u2013420 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"28_CR14","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/0020-0190(79)90071-1","volume":"9","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N.: A note on simplification orderings. Information Processing Letters\u00a09(5), 212\u2013215 (1979)","journal-title":"Information Processing Letters"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1007\/3-540-10843-2_36","volume-title":"Automata, Languages and Programming","author":"N. Dershowitz","year":"1981","unstructured":"Dershowitz, N.: Termination of linear rewriting systems. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol.\u00a0115, pp. 448\u2013458. Springer, Heidelberg (1981)"},{"key":"28_CR16","first-page":"3","volume-title":"Proceedings of the International Logic Programming Symposium","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N.: Goal solving as operational semantics. In: Proceedings of the International Logic Programming Symposium, Portland, OR, pp. 3\u201317. MIT Press, Cambridge (1995)"},{"issue":"2","key":"28_CR17","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N., Hoot, C.: Natural termination. Theoretical Computer Science\u00a0142(2), 179\u2013207 (1995)","journal-title":"Theoretical Computer Science"},{"key":"28_CR18","series-title":"Formal Methods and Semantics","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Methods and Semantics, vol.\u00a0B, ch. 6, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/3-540-53904-2_120","volume-title":"Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1991","unstructured":"Dershowitz, N., Jouannaud, J.-P., Klop, J.W.: Open problems in rewriting. In: Book, R.V. (ed.) RTA 1991. LNCS, vol.\u00a0488, pp. 445\u2013456. Springer, Heidelberg (1991)"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"468","DOI":"10.1007\/3-540-56868-9_39","volume-title":"Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1993","unstructured":"Dershowitz, N., Jouannaud, J.-P., Klop, J.W.: More problems in rewriting. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 468\u2013487. Springer, Heidelberg (1993)"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/3-540-59200-8_82","volume-title":"Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1995","unstructured":"Dershowitz, N., Jouannaud, J.-P., Klop, J.W.: Problems in rewriting III. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 457\u2013471. Springer, Heidelberg (1995)"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theoretical Computer Science (to appear)","DOI":"10.1016\/j.tcs.2006.03.012"},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/BFb0052380","volume-title":"Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1998","unstructured":"Dershowitz, N., Treinen, R.: An on-line problem database. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 332\u2013342. Springer, Heidelberg (1998)"},{"key":"28_CR24","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1017\/S0305004100027092","volume":"47","author":"T. Evans","year":"1951","unstructured":"Evans, T.: On multiplicative systems defined by generators and relations, I. Proceedings of the Cambridge Philosophical Society\u00a047, 637\u2013649 (1951)","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"28_CR25","unstructured":"Geser, A.: A solution to Zantema\u2019s problem. Technical Report MIP-9314, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau (1993)"},{"key":"28_CR26","unstructured":"Geser, A.: Termination of one-rule string rewriting systems _ \u2192 r where |r| \u2264 9. Technical report, Wilhelm-Schickard-Institut, Universit\u00e4t T\u00fcbingen, Germany (January 1998)"},{"key":"28_CR27","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1016\/S0304-3975(00)00167-5","volume":"243","author":"A. Geser","year":"2000","unstructured":"Geser, A.: Note on normalizing, non-terminating one-rule string rewriting systems. Theoretical Computer Science\u00a0243, 489\u2013498 (2000)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"28_CR28","doi-asserted-by":"publisher","first-page":"1156","DOI":"10.1137\/S009753979833297X","volume":"31","author":"A. Geser","year":"2002","unstructured":"Geser, A.: Decidability of termination of grid string rewriting rules. SIAM J. Comput.\u00a031(4), 1156\u20131168 (2002)","journal-title":"SIAM J. Comput."},{"key":"28_CR29","unstructured":"Geser, A.: Is Termination Decidable for String Rewriting with Only One Rule? Habilitation thesis, Universit\u00e4t T\u00fcbingen, Germany (January 2002)"},{"key":"28_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-44881-0_29","volume-title":"Rewriting Techniques and Applications","author":"A. Geser","year":"2003","unstructured":"Geser, A.: Termination of string rewriting rules that have one pair of overlaps. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 410\u2013423. Springer, Heidelberg (2003)"},{"key":"28_CR31","doi-asserted-by":"crossref","unstructured":"Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. J. Automat. Reason (to appear)","DOI":"10.1007\/s10817-005-9024-8"},{"key":"28_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BFb0030600","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"A. Geser","year":"1997","unstructured":"Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H.: Relative undecidability in the termination hierarchy of single rewrite rules. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 237\u2013248. Springer, Heidelberg (1997)"},{"issue":"1","key":"28_CR33","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1006\/inco.2002.3120","volume":"178","author":"A. Geser","year":"2002","unstructured":"Geser, A., Middeldorp, A., Ohlebusch, E., Zantema, H.: Relative undecidability in term rewriting, Part I: The termination hierarchy. Inform. and Computation\u00a0178(1), 101\u2013131 (2002)","journal-title":"Inform. and Computation"},{"issue":"3","key":"28_CR34","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1051\/ita:1999118","volume":"33","author":"A. Geser","year":"1999","unstructured":"Geser, A., Zantema, H.: Non-looping string rewriting. Theoret. Informatics Appl.\u00a033(3), 279\u2013301 (1999)","journal-title":"Theoret. Informatics Appl."},{"key":"28_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36494-3_9","volume-title":"STACS 2003","author":"G. Godoy","year":"2003","unstructured":"Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 85\u201396. Springer, Heidelberg (2003)"},{"issue":"6","key":"28_CR36","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1016\/0016-0032(73)90303-7","volume":"296","author":"S. Gorn","year":"1973","unstructured":"Gorn, S.: On the conclusive validation of symbol manipulation processes (how do you know it has to work?). J. of the Franklin Institute\u00a0296(6), 499\u2013518 (1973)","journal-title":"J. of the Franklin Institute"},{"key":"28_CR37","doi-asserted-by":"crossref","unstructured":"Gorn, S.: Handling the growth by definition of mechanical languages. In: Proceedings of the Spring Joint Computer Conference, Philadelphia, PA, Spring, pp. 213\u2013224 (1967)","DOI":"10.1145\/1465482.1465513"},{"key":"28_CR38","unstructured":"Gramlich, B.: Relating innermost, weak, uniform and modular termination of term rewriting systems. SEKI-Report SR-93-09, Fachbereich Informatik, Universit\u00e4t Kaiserslautern, Kaiserslautern, West Germany (1993)"},{"key":"28_CR39","doi-asserted-by":"crossref","unstructured":"Gramlich, B.: Confluence without termination via parallel critical pairs. In: Colloquium on Trees in Algebra and Programming, pp. 211\u2013225 (1996)","DOI":"10.1007\/3-540-61064-2_39"},{"issue":"7","key":"28_CR40","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society (3),\u00a02(7), 326\u2013336 (1952)","journal-title":"Proceedings of the London Mathematical Society (3)"},{"key":"28_CR41","unstructured":"Roger Hindley, J.: The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne (1964)"},{"key":"28_CR42","unstructured":"Hofbauer, D., Waldmann, J.: Deleting string rewriting systems preserve regularity. Theoretical Computer Science (to appear)"},{"key":"28_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Automata, Languages and Programming","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 54\u201371. Springer, Heidelberg (1987)"},{"issue":"4","key":"28_CR44","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery\u00a027(4), 797\u2013821 (1980)","journal-title":"J. of the Association for Computing Machinery"},{"key":"28_CR45","unstructured":"Huet, G., Lankford, D.S.: On the uniform halting problem for term rewriting systems. Rapport laboria 283, Institut de Recherche en Informatique et en Automatique, Le Chesnay, France (March 1978)"},{"key":"28_CR46","unstructured":"Huet, G., L\u00e9vy, J.-J.: Call by need computations in non-ambiguous linear term rewriting systems. Rapport Laboria 359, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France (August 1979)"},{"key":"28_CR47","first-page":"395","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"G. Huet","year":"1991","unstructured":"Huet, G., L\u00e9vy, J.-J.: Computations in orthogonal rewriting systems, I and II. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 395\u2013443. The MIT Press, Cambridge (1991); This is a revision of [46]"},{"issue":"3","key":"28_CR48","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1051\/ita\/1984180301911","volume":"18","author":"J.-P. Jouannaud","year":"1984","unstructured":"Jouannaud, J.-P., Kirchner, H.: Construction d\u2019un plus petit ordre de simplification. RAIRO Theoretical Informatics\u00a018(3), 191\u2013207 (1984)","journal-title":"RAIRO Theoretical Informatics"},{"key":"28_CR49","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"4","author":"D. Kapur","year":"1988","unstructured":"Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered for the Knuth-Bendix procedure. J. Symbolic Computation\u00a04, 19\u201336 (1988)","journal-title":"J. Symbolic Computation"},{"issue":"1\u20133","key":"28_CR50","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0304-3975(02)00570-4","volume":"301","author":"M. Katsura","year":"2003","unstructured":"Katsura, M., Kobayashi, Y., Otto, F.: Undecidable properties of monoids with word problem solvable in linear time. Part II\u2013 Cross sections and homological and homotopical finiteness conditions. Theoretical Computer Science\u00a0301(1\u20133), 79\u2013101 (2003)","journal-title":"Theoretical Computer Science"},{"key":"28_CR51","unstructured":"Klop, J.W.: Combinatory Reduction Systems, Mathematisch Centrum, Amsterdam. Mathematical Centre Tracts, vol.\u00a0127 (1980)"},{"key":"#cr-split#-28_CR52.1","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263???297. Pergamon Press, Oxford (1970);","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"#cr-split#-28_CR52.2","unstructured":"Reprinted in Automation of Reasoning 2, pp. 342???376. Springer, Berlin (1983)"},{"issue":"1\/2","key":"28_CR53","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(00)00367-4","volume":"262","author":"Y. Kobayashi","year":"2001","unstructured":"Kobayashi, Y., Katsura, M., Shikishima-Tsuji, K.: Termination and derivational complexity of confluent one-rule string rewriting systems. Theoretical Computer Science\u00a0262(1\/2), 583\u2013632 (2001)","journal-title":"Theoretical Computer Science"},{"key":"28_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-15984-3_294","volume-title":"EUROCAL \u201985. European Conference on Computer Algebra. Linz, Austria, April 1-3, 1985. Proceedings","author":"W. K\u00fcchlin","year":"1985","unstructured":"K\u00fcchlin, W.: A confluence criterion based on the generalized Newman Lemma. In: Caviness, B.F. (ed.) ISSAC 1985 and EUROCAL 1985. LNCS, vol.\u00a0204, pp. 390\u2013399. Springer, Heidelberg (1985)"},{"key":"28_CR55","unstructured":"Kurth, W.: Termination und Konfluenz von Semi-Thue-Systems mit nur einer Regel. PhD thesis, Technische Universitat Clausthal, Clausthal, Germany (1990) (in German)"},{"key":"28_CR56","first-page":"355","volume":"30","author":"W. Kurth","year":"1996","unstructured":"Kurth, W.: One-rule semi-Thue systems with loops of length one, two, or three. Inform. The\u00e9or. Appl.\u00a030, 355\u2013268 (1996)","journal-title":"Inform. The\u00e9or. Appl."},{"key":"28_CR57","unstructured":"Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX (December 1975)"},{"key":"28_CR58","unstructured":"Lankford, D.S., Musser, D.R.: A finite termination criterion (May 1978)"},{"issue":"1-2","key":"28_CR59","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/0304-3975(94)00029-8","volume":"132","author":"P. Lescanne","year":"1994","unstructured":"Lescanne, P.: On termination of one rule rewrite systems. Theoretical Computer Science\u00a0132(1-2), 395\u2013401 (1994)","journal-title":"Theoretical Computer Science"},{"key":"28_CR60","unstructured":"Lipton, R., Snyder, L.: On the halting of tree replacement systems. In: Proceedings of the Conference on Theoretical Computer Science, Waterloo, Canada, August 1977, pp. 43\u201346 (1977)"},{"key":"#cr-split#-28_CR61.1","unstructured":"McNaughton, R.: The uniform halting problem for one-rule semi-Thue systems. Technical Report 94-18, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY (August 1994);"},{"key":"#cr-split#-28_CR61.2","unstructured":"Correction (August 1996)"},{"key":"#cr-split#-28_CR62.1","unstructured":"McNaughton, R.: Well-behaved derivations in one-rule semi-Thue systems. Technical Report 95-15, Dept. of Computer Science, Rensselaer Polytechnic Institute, Troy, NY (November 1995);"},{"key":"#cr-split#-28_CR62.2","unstructured":"Correction (July 1996)"},{"issue":"1","key":"28_CR63","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/S0304-3975(98)00053-X","volume":"207","author":"R. McNaughton","year":"1998","unstructured":"McNaughton, R.: Contributions of Ronald V. Book to the theory of stringrewriting systems. Theor. Comput. Sci.\u00a0207(1), 13\u201323 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"28_CR64","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1023\/A:1010759024900","volume":"26","author":"R. McNaughton","year":"2001","unstructured":"McNaughton, R.: Semi-Thue systems with an inhibitor. Journal of Automated Reasoning\u00a026(4), 409\u2013431 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR65","unstructured":"Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, Honolulu, HI, January 1970, pp. 789\u2013792 (1970)"},{"key":"28_CR66","unstructured":"Markov, A.A.: Theory of Algorithms. Moscow (1954)"},{"issue":"2","key":"28_CR67","first-page":"555","volume":"8","author":"J.V. Matiyasevich","year":"1967","unstructured":"Matiyasevich, J.V.: Simple examples of undecidable associative calculi. Soviet Mathematics (Dokladi)\u00a08(2), 555\u2013557 (1967)","journal-title":"Soviet Mathematics (Dokladi)"},{"key":"28_CR68","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1109\/LICS.1996.561469","volume-title":"Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science","author":"Y. Matiyasevich","year":"1996","unstructured":"Matiyasevich, Y., S\u00e9nizergues, G.: Decision problems for semi-Thue systems with a few rules. In: Clarke, E. (ed.) Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, July 1996, pp. 523\u2013531. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"28_CR69","unstructured":"Matsumoto, T.: On confluence conditions of left-linear term rewriting systems. Master\u2019s thesis, School of Information Science, Japan Advanced Institute of Science and Technology (February 2000) (in Japanese), English abstract is available at, http:\/\/www.jaist.ac.jp\/library\/thesis\/is-master-2000\/paper\/tmatsumo\/abstract.pdf"},{"issue":"1","key":"28_CR70","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(85)90006-4","volume":"35","author":"Y. M\u00e9tivier","year":"1985","unstructured":"M\u00e9tivier, Y.: Calcul de longueurs de cha\u00eenes de r\u00e9\u00e9criture dans le mono\u00efde libre. Theoretical Computer Science\u00a035(1), 71\u201387 (1985)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"28_CR71","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF01225647","volume":"6","author":"A. Middeldorp","year":"1995","unstructured":"Middeldorp, A., Gramlich, B.: Simple termination is difficult. Applied Algebra on Engineering, Communication and Computer Science\u00a06(2), 115\u2013128 (1995)","journal-title":"Applied Algebra on Engineering, Communication and Computer Science"},{"key":"28_CR72","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. of the Sixteenth International Conf. on Rewriting Techniques and Applications","author":"W. Moczyd\u0142owski Jr.","year":"2005","unstructured":"Moczyd\u0142owski Jr., W., Geser, A.: Termination of single-threaded onerule semi-Thue systems. In: Proc. of the Sixteenth International Conf. on Rewriting Techniques and Applications, Nara, Japan, April 2005. LNCS, Springer, Heidelberg (2005)"},{"issue":"2","key":"28_CR73","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. Herman","year":"1942","unstructured":"Herman, M., Newman, A.: On theories with a combinatorial definition of \u2018equivalence\u2019. Annals of Mathematics\u00a043(2), 223\u2013243 (1942)","journal-title":"Annals of Mathematics"},{"key":"28_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/BFb0052357","volume-title":"Rewriting Techniques and Applications","author":"S. Okui","year":"1998","unstructured":"Okui, S.: Simultaneous critical pairs and Church-Rosser property. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 2\u201316. Springer, Heidelberg (1998)"},{"issue":"2","key":"28_CR75","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/0304-3975(92)00023-K","volume":"126","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V.: Confluence by decreasing diagrams. Theoretical Computer Science\u00a0126(2), 259\u2013280 (1994)","journal-title":"Theoretical Computer Science"},{"key":"28_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-61254-8_26","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V. Oostrom van","year":"1996","unstructured":"van Oostrom, V.: Development closed critical pairs. In: Dowek, G., Heering, J., Meinke, K., M\u00f6ller, B. (eds.) HOA 1995. LNCS, vol.\u00a01074, pp. 185\u2013200. Springer, Heidelberg (1996)"},{"key":"28_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-62950-5_70","volume-title":"Rewriting Techniques and Applications","author":"M. Oyamaguchi","year":"1997","unstructured":"Oyamaguchi, M., Ohta, Y.: A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 187\u2013201. Springer, Heidelberg (1997)"},{"issue":"2","key":"28_CR78","first-page":"290","volume":"E87- D","author":"M. Oyamaguchi","year":"2004","unstructured":"Oyamaguchi, M., Ohta, Y.: On the open problems concerning Church-Rosser of left-linear term rewriting systems. Trans. of IEICE\u00a0E87- D(2), 290\u2013298 (2004)","journal-title":"Trans. of IEICE"},{"issue":"2","key":"28_CR79","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1006\/inco.1996.0028","volume":"125","author":"D.A. Plaisted","year":"1996","unstructured":"Plaisted, D.A., Sattler-Klein, A.: Proof lengths for equational completion. Information and Computation\u00a0125(2), 154\u2013170 (1996)","journal-title":"Information and Computation"},{"issue":"1","key":"28_CR80","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Alan Robinson","year":"1965","unstructured":"Alan Robinson, J.: A machine-oriented logic based on the resolution principle. J. of the Association for Computing Machinery\u00a012(1), 23\u201341 (1965)","journal-title":"J. of the Association for Computing Machinery"},{"issue":"1","key":"28_CR81","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1145\/321738.321750","volume":"20","author":"B. Rosen","year":"1973","unstructured":"Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. J. of the Association for Computing Machinery\u00a020(1), 160\u2013187 (1973)","journal-title":"J. of the Association for Computing Machinery"},{"key":"28_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-61464-8_61","volume-title":"Rewriting Techniques and Applications","author":"G. S\u00e9nizergues","year":"1996","unstructured":"S\u00e9nizergues, G.: On the termination problem for one-rule semi-Thue systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 302\u2013316. Springer, Heidelberg (1996)"},{"issue":"2","key":"28_CR83","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0020-0190(96)00200-1","volume":"61","author":"K. Shikishima-Tsuji","year":"1997","unstructured":"Shikishima-Tsuji, K., Katsura, M., Kobayashi, Y.: On termination of confluent one-rule string-rewriting systems. Inf. Process. Lett.\u00a061(2), 91\u201396 (1997)","journal-title":"Inf. Process. Lett."},{"key":"28_CR84","unstructured":"Socher-Ambrosius, R.: On the Church-Rosser property in left-linear systems. Technical Report TR 91\/17, SUNY at Stony Brook (1991)"},{"key":"28_CR85","first-page":"256","volume":"72","author":"M. Steinby","year":"2000","unstructured":"Steinby, M., Thomas, W.: Trees and term rewriting in 1910: On a paper by Axel Thue. Bulletin of the European Association for Theoretical Computer Science\u00a072, 256\u2013269 (2000)","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"28_CR86","first-page":"1201","volume":"323","author":"E.T. Bittar","year":"1996","unstructured":"Bittar, E.T.: Complexit\u00e9 lin\u00e9aire du probl\u00e8me de Zantema. Comptes Rendus de l\u2019Acad\u00e9mie des Sciences, Paris\u00a0323, 1201\u20131206 (1996)","journal-title":"Comptes Rendus de l\u2019Acad\u00e9mie des Sciences, Paris"},{"issue":"1","key":"28_CR87","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in \u03bb-calculus. Information and Computation\u00a0118(1), 120\u2013127 (1995)","journal-title":"Information and Computation"},{"volume-title":"\u201cTerese\u201d Term Rewriting Systems.","year":"2002","key":"28_CR88","unstructured":"Bezem, M., Klop, J.W., de Vrijer, R. (eds.): \u201cTerese\u201d Term Rewriting Systems. Cambridge University Press, Cambridge (2002)"},{"key":"28_CR89","unstructured":"Thue, A.: Die L\u00f6sung eines Spezialfalles eines generellen logischen Problems. Kra. Videnskabs-Selskabets Skrifter I. Mat. Nat. Kl. (8) (1910)"},{"key":"28_CR90","unstructured":"Thue, A.: Probleme \u00fcber Veranderungen von Zeichenreihen nach gegeben Regeln. Skr. Vid. Kristianaia I. Mat. Naturv. Klasse, 10\/34 (1914)"},{"key":"28_CR91","unstructured":"Toyama, Y.: On the Church-Rosser property of term rewriting systems. ECL Technical Report 17672, NTT (December 1981)(In Japanese); English pr\u00e9cis, \u201cOn parallel critical pairs\u201d (November 1995)"},{"key":"28_CR92","first-page":"393","volume-title":"Programming of Future Generation Computers II","author":"Y. Toyama","year":"1988","unstructured":"Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, pp. 393\u2013407. North-Holland, Amsterdam (1988)"},{"key":"28_CR93","doi-asserted-by":"crossref","unstructured":"Winkler, F., Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Proceedings of the Colloquium on Algebra, Combinatorics and Logic in Computer Science, Gy\u00f6r, Hungary (September 1983)","DOI":"10.1145\/1089338.1089341"},{"key":"28_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/3-540-55124-7_11","volume-title":"Word Equations and Related Topics","author":"C. Wrathall","year":"1992","unstructured":"Wrathall, C.: Confluence of one-rule Thue systems. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol.\u00a0572, pp. 237\u2013246. Springer, Heidelberg (1992)"},{"key":"28_CR95","volume-title":"Recursive Function Theory and Logic","author":"A. Yasuhara","year":"1971","unstructured":"Yasuhara, A.: Recursive Function Theory and Logic. Academic Press, London (1971)"},{"issue":"1","key":"28_CR96","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1006\/jsco.1995.1037","volume":"20","author":"H. Zantema","year":"1995","unstructured":"Zantema, H.: Total termination of term rewriting is undecidable. Journal of Symbolic Computation\u00a020(1), 43\u201360 (1995)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"28_CR97","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s002009900019","volume":"11","author":"H. Zantema","year":"2000","unstructured":"Zantema, H., Geser, A.: A complete characterization of termination of 0p1q \u2192 1r0s. Applicable Algebra in Engineering, Communication, and Computing\u00a011(1), 1\u201325 (2000)","journal-title":"Applicable Algebra in Engineering, Communication, and Computing"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:34:00Z","timestamp":1605760440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":100,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}