{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:21:57Z","timestamp":1725495717420},"publisher-location":"Berlin, Heidelberg","reference-count":87,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052380","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T05:31:11Z","timestamp":1149658271000},"page":"332-342","source":"Crossref","is-referenced-by-count":1,"title":["An on-line problem database"],"prefix":"10.1007","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Treinen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"25_CR1","volume-title":"Proceedings of the Eleventh International Conference on Automated Deduction (Saratoga Springs, NY), volume 607 of Lecture Notes in Artificial Intelligence","author":"F. Baader","year":"1992","unstructured":"F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In D. Kapur, editor, Proceedings of the Eleventh International Conference on Automated Deduction (Saratoga Springs, NY), volume 607 of Lecture Notes in Artificial Intelligence, Berlin, June 1992. Springer-Verlag."},{"key":"25_CR2","first-page":"352","volume-title":"Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Artificial Intelligence","author":"F. Baader","year":"1995","unstructured":"F. Baader and K. Schulz. Combination of constraint solving techniques: An algebraic point of view. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Artificial Intelligence, pages 352\u2013366, Kaiserslautern, Germany, 1995. Springer Verlag."},{"key":"25_CR3","volume-title":"Proceedings of the International Conference on Principles and Practice of Constraint Programming, CP95, volume 976 of Lecture Notes in Artificial Intelligence","author":"F. Baader","year":"1995","unstructured":"F. Baader and K. Schulz. On the combination of symbolic constraints, solution domains, and constraint solvers. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, CP95, volume 976 of Lecture Notes in Artificial Intelligence, Cassis, France, 1995. Springer Verlag."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"F. Baader and K. Schulz. Combination of constraint solvers for free and quasi-free structures. Theoretical Computer Science, 1998. To appear.","DOI":"10.1016\/S0304-3975(97)00147-3"},{"key":"25_CR5","volume-title":"The Lambda Calculus, its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North-Holland, Amsterdam, second edition, 1984.","edition":"second edition"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"M. Bidoit and M. Dauchet, editors. Theory and Practice of Software Development, Lecture Notes in Computer Science, vol. 1214, Lille, France, April 1997. Springer-Verlag.","DOI":"10.1007\/BFb0030581"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"H. Bunke, T. Glauser, and T.-H. Tran. An efficient implementation of graph grammars based on the RETE-matching algorithm. In H. Ehrig, H.-J. Kreowski, and G. Rozenberg, editors, Graph Grammars and Their Application to Computer Science, volume 532 of Lecture Notes in Computer Science, pages 174\u2013189, 1991.","DOI":"10.1007\/BFb0017389"},{"key":"25_CR8","first-page":"74","volume-title":"Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 1: Colloquium on Trees in Algebra and Programming (Brighton, U.K.), volume 493 of Lecture Notes in Computer Science","author":"A.-C. Caron","year":"1991","unstructured":"A.-C. Caron. Linear bounded automata and rewrite systems: Influence of initial configurations on decision properties. In Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 1: Colloquium on Trees in Algebra and Programming (Brighton, U.K.), volume 493 of Lecture Notes in Computer Science, pages 74\u201389, Berlin, April 1991. Springer-Verlag."},{"key":"25_CR9","volume-title":"Proceedings of the Fifth International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science","author":"A.-C. Caron","year":"1993","unstructured":"A.-C. Caron, J.-L. Coquid\u00e9, and M. Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, Proceedings of the Fifth International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, Montreal, Canada, 1993. Springer-Verlag."},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"P. Chew. Unique normal forms in term rewriting systems with repeated variables. In Proceedings of the Thirteenth Annual Symposium on Theory of Computing, pages 7\u201318. ACM, 1981.","DOI":"10.1145\/800076.802452"},{"key":"25_CR11","unstructured":"H. Comon. Unification et Disunification: Th\u00e9orie et Applications. PhD thesis, l'Institut National Polytechnique de Grenoble, 1988."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"H. Comon, editor. 8th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1232, Sitges, Spain, June 1997. Springer-Verlag.","DOI":"10.1007\/3-540-62950-5"},{"key":"25_CR13","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/LICS.1997.614922","volume-title":"Twelfth Annual IEEE Symposium on Logic in Computer Science","author":"H. Comon","year":"1997","unstructured":"H. Comon and F. Jacquemard. Ground reducibility is EXPTIME-complete. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 26\u201334, Warsaw,Poland, June 1997. IEEE."},{"key":"25_CR14","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0304-3975(94)90268-2","volume":"126","author":"B. Courcelle","year":"1994","unstructured":"B. Courcelle. Monadic-second order graph transductions: A survey. Theoretical Computer Science, 126:53\u201375, 1994.","journal-title":"Theoretical Computer Science"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1142\/9789812384720_0005","volume-title":"Handbook of graph grammars and computing by graph transformations, vol. 1: Foundations","author":"B. Courcelle","year":"1997","unstructured":"B. Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In G. Rozenberg, editor, Handbook of graph grammars and computing by graph transformations, vol. 1: Foundations, chapter 5, pages 313\u2013400. World Scientific, New-Jersey, London, 1997."},{"key":"25_CR16","unstructured":"P.-L. Curien, T. Hardin, and J.-J. Levy. Confluence properties of weak and strong calculi of explicit substitutions. RR 1617, Institut National de Rechereche en Informatique et en Automatique, Rocquencourt, February 1992."},{"key":"25_CR17","first-page":"109","volume-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC), volume 355 of Lecture Notes in Computer Science","author":"M. Dauchet","year":"1989","unstructured":"M. Dauchet. Simulation of Turing machines by a left-linear rewrite rule. In N. Dershowitz, editor, Proceedings of the Third International Conference on Rewriting Techniques and Applications (Chapel Hill, NC), volume 355 of Lecture Notes in Computer Science, pages 109\u2013120, Berlin, April 1989. Springer-Verlag."},{"issue":"2","key":"25_CR18","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1016\/0304-3975(92)90022-8","volume":"103","author":"M. Dauchet","year":"1992","unstructured":"M. Dauchet. Simulation of Turing machines by a regular rewrite rule. Theoretical Computer Science, 103(2):409\u2013420, 1992.","journal-title":"Theoretical Computer Science"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"N. Dershowitz. Innocuous constructor-sharing combinations. In Comon [12], pages 202\u2013216.","DOI":"10.1007\/3-540-62950-5_71"},{"key":"25_CR20","first-page":"243","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243\u2013320. North-Holland, Amsterdam, 1990."},{"key":"25_CR21","first-page":"445","volume-title":"Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), volume 488 of Lecture Notes in Computer Science","author":"N. Dershowitz","year":"1991","unstructured":"N. Dershowitz, J.-P. Jouannaud, and J. W. Klop. Open problems in rewriting. In R. Book, editor, Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), volume 488 of Lecture Notes in Computer Science, pages 445\u2013456, Berlin, April 1991. Springer-Verlag."},{"key":"25_CR22","first-page":"468","volume-title":"Proceedings of the Fifth International Conference on Rewriting Techniques and Applications (Montreal, Canada), volume 690 of Lecture Notes in Computer Science","author":"N. Dershowitz","year":"1993","unstructured":"N. Dershowitz, J.-P. Jouannaud, and J. W. Klop. More problems in rewriting. In C. Kirchner, editor, Proceedings of the Fifth International Conference on Rewriting Techniques and Applications (Montreal, Canada), volume 690 of Lecture Notes in Computer Science, pages 468\u2013487, Berlin, June 1993. Springer-Verlag."},{"key":"25_CR23","volume-title":"Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany), Lecture Notes in Computer Science","author":"N. Dershowitz","year":"1995","unstructured":"N. Dershowitz, J.-P. Jouannaud, and J. W. Klop. Problems in rewriting III. In Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany), Lecture Notes in Computer Science, Berlin, April 1995. Springer-Verlag."},{"key":"25_CR24","first-page":"267","volume-title":"CADE 94, volume 814 of Lecture Notes in Artificial Intelligence","author":"E. Domenjoud","year":"1994","unstructured":"E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for nondisjoint equational theories. In A. Bundy, editor, CADE 94, volume 814 of Lecture Notes in Artificial Intelligence, pages 267\u2013281, Nancy, France, 1994. Springer-Verlag."},{"key":"25_CR25","unstructured":"R. Freese. personal communication, 1993."},{"volume-title":"Lecture Notes in Computer Science, vol. 1103","year":"1996","key":"25_CR26","unstructured":"H. Ganzinger, editor. 7th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 1103, New Brunswick, NJ, USA, July 1996. Springer-Verlag."},{"key":"25_CR27","volume-title":"PhD thesis","author":"A. Geser","year":"1990","unstructured":"A. Geser. Relative Termination. PhD thesis, Universit\u00e4t Passau, Passau, Germany, 1990."},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"A. Geser, A. Middeldorp, E. Ohlebusch, and H. Zantema. Relative undecidability in the termination hierarchy of single rewrite rules. In Bidoit and Dauchet [6], pages 237\u2013248.","DOI":"10.1007\/BFb0030600"},{"issue":"4","key":"25_CR29","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery, 27(4):797\u2013821, October 1980.","journal-title":"J. of the Association for Computing Machinery"},{"key":"25_CR30","unstructured":"G. Huet and D. S. Lankford. 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."},{"issue":"1","key":"25_CR31","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1997.2633","volume":"137","author":"B. Intrigila","year":"1997","unstructured":"B. Intrigila. Non-existent statman's double fixed point combinator does not exist, indeed. Information and Computation, 137(1):35\u201340, 1997.","journal-title":"Information and Computation"},{"key":"25_CR32","unstructured":"F. Jacquemard. fr Automates d'arbres et R\u00e9\u00e9criture de termes. PhD thesis, Universit\u00e9 de Paris-Sud, 1996. In French."},{"issue":"3","key":"25_CR33","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1051\/ita\/1984180301911","volume":"18","author":"J.-P. Jouannaud","year":"1984","unstructured":"J.-P. Jouannaud and H. Kirchner. Construction d'un plus petit ordre de simplification. RAIRO Theoretical Informatics, 18(3):191\u2013207, 1984.","journal-title":"RAIRO Theoretical Informatics"},{"issue":"4","key":"25_CR34","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"D. Kapur, P. Narendran, and H. Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395\u2013415, August 1987.","journal-title":"Acta Informatica"},{"key":"25_CR35","volume-title":"Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts","author":"J. W. Klop","year":"1980","unstructured":"J. W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980."},{"key":"25_CR36","first-page":"1","volume-title":"Handbook of Logic in Computer Science, volume 2","author":"J. W. Klop","year":"1992","unstructured":"J. W. Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1\u2013117. Oxford University Press, Oxford, 1992."},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Y. Kobayashi, M. Katsura, and K. Shikishima-Tsuji. Termination and derivational complexity of confluent one-rule string-rewriting systems. Technical report, Toho university, Japan, 1997.","DOI":"10.1016\/S0020-0190(96)00200-1"},{"key":"25_CR38","first-page":"210","volume":"95","author":"J. B. Kruskal","year":"1960","unstructured":"J. B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210\u2013225, May 1960.","journal-title":"Transactions of the American Mathematical Society"},{"key":"25_CR39","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0304-3975(92)90015-8","volume":"103","author":"M. Kurihara","year":"1992","unstructured":"M. Kurihara and A. Ohuchi. Modularity of simple termination of term rewriting systems with shared constructors. Theoretical Computer Science, 103:273\u2013282, 1992.","journal-title":"Theoretical Computer Science"},{"key":"25_CR40","volume-title":"PhD thesis","author":"W. Kurth","year":"1990","unstructured":"W. Kurth. Termination und Konfluenz von Semi-Thue-Systems mit nur einer Regel. PhD thesis, Technische Universitat Clausthal, Clausthal, Germany, 1990. In German."},{"key":"25_CR41","first-page":"409","volume":"132","author":"P. Lescanne","year":"1992","unstructured":"P. Lescanne. On termination of one rule rewrite systems. Theoretical Computer Science, 132:409\u2013420, 1992.","journal-title":"Theoretical Computer Science"},{"key":"25_CR42","unstructured":"P. Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions \u03bb\u03c5. Technical Report RR-2222, INRIA-Lorraine, January 1994."},{"key":"25_CR43","unstructured":"I. Litovski, Y. M\u00e9tivier, and E. Sopena. Definitions and comparisons of local computations on graphs. Mathematical Systems Theory, to appear. Available as internal report 91-43 of LaBRI, University of Bordeaux 1."},{"key":"25_CR44","first-page":"348","volume-title":"Proceedings of the Third IEEE Symposium on Logic in Computer Science","author":"M. J. Maher","year":"1988","unstructured":"M. J. Maher. Complete axiomatizations of the algebras of the finite, rational and infinite trees. In Proceedings of the Third IEEE Symposium on Logic in Computer Science, pages 348\u2013357, Edinburgh, UK, July 1988. IEEE, Computer Society Press."},{"key":"25_CR45","unstructured":"K. Mano and M. Ogawa. A new proof of Chew's theorem. Technical report, IPSJ PRG94-19-7, 1994."},{"key":"25_CR46","doi-asserted-by":"crossref","unstructured":"J. Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. In Comon [12], pages 241\u2013253.","DOI":"10.1007\/3-540-62950-5_75"},{"key":"25_CR47","unstructured":"A. Martelli and G. Rossi. Efficient unification with infinite terms in logic programming. In International conference on fifth generation computer systems, pages 202\u2013209, 1984."},{"key":"25_CR48","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate, 1995. To appear.","DOI":"10.1007\/BFb0014062"},{"issue":"2","key":"25_CR49","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF01225647","volume":"6","author":"A. Middeldorp","year":"1995","unstructured":"A. Middeldorp and B. Gramlich. Simple termination is difficult. Applicable Algebra in Engineering, Communication and Computing, 6(2):115\u2013128, 1995.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"25_CR50","first-page":"174","volume-title":"Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), volume 488 of Lecture Notes in Computer Science","author":"A. Middeldorp","year":"1991","unstructured":"A. Middeldorp and Y. Toyama. Completeness of combinations of constructor systems. In R. Book, editor, Proceedings of the Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), volume 488 of Lecture Notes in Computer Science, pages 174\u2013187, Berlin, April 1991. Springer-Verlag."},{"key":"25_CR51","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1109\/LICS.1996.561460","volume-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science","author":"C. Mu\u00f1oz","year":"1996","unstructured":"C. Mu\u00f1oz. Confluence and preservation of strong normalisation in an explicit substitutions calculus (extended abstract). In Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 440\u2013447, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press."},{"key":"25_CR52","doi-asserted-by":"crossref","unstructured":"J. Niehren, M. Pinkal, and P. Ruhrberg. On equality up-to constraints over finite trees, context unification and one-step rewriting. In 14th International Conference on Automated Deduction, Townsville, Australia, July 1997. To appear.","DOI":"10.1007\/3-540-63104-6_4"},{"key":"25_CR53","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1109\/LICS.1991.151658","volume-title":"Proceedings of the Sixth Symposium on Logic in Computer Science","author":"T. Nipkow","year":"1991","unstructured":"T. Nipkow. Higher-order critical pairs. In Proceedings of the Sixth Symposium on Logic in Computer Science, pages 342\u2013349, Amsterdam, The Netherlands, 1991. IEEE."},{"key":"25_CR54","unstructured":"M. Ogawa and S. Ono. On the uniquely converging property of nonlinear term rewriting systems. Technical report, IEICE COMP89-7, 1989."},{"key":"25_CR55","doi-asserted-by":"crossref","unstructured":"E. Ohlebusch. On the modularity of confluence of constructor-sharing term rewriting systems. In 19th Colloquium on Trees in Algebra and Programming, volume 787 of LNCS, pages 261\u2013275. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0017487"},{"key":"25_CR56","doi-asserted-by":"crossref","unstructured":"E. Ohlebusch. On the modularity of confluence of constructor-sharing term rewriting systems. In Proceedings of the Colloquium on Trees in Algebra and Programming, 1994.","DOI":"10.1007\/BFb0017487"},{"key":"25_CR57","volume-title":"PhD thesis","author":"V. v. Oostrom","year":"1994","unstructured":"V. v. Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994."},{"key":"25_CR58","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"V. v. Oostrom","year":"1997","unstructured":"V. v. Oostrom. Developing developments. Theoretical Computer Science, 175:159\u2013181, 1997.","journal-title":"Theoretical Computer Science"},{"key":"25_CR59","first-page":"39","volume":"J76-D-I","author":"M. Oyamaguchi","year":"1993","unstructured":"M. Oyamaguchi and Y. Ohta. On the confluent property of right-ground term rewriting systems. Trans. IEICE, J76-D-I:39\u201345, 1993.","journal-title":"Trans. IEICE"},{"key":"25_CR60","doi-asserted-by":"crossref","unstructured":"M. Oyamaguchi and Y. Ohta. A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In Comon [12], pages 187\u2013201.","DOI":"10.1007\/3-540-62950-5_70"},{"issue":"2\/3","key":"25_CR61","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. A. Plaisted","year":"1985","unstructured":"D. A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65(2\/3):182\u2013215, May\/June 1985.","journal-title":"Information and Control"},{"key":"25_CR62","volume-title":"PhD thesis","author":"F. v. Raamsdonk","year":"1996","unstructured":"F. v. Raamsdonk. Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1996."},{"key":"25_CR63","unstructured":"M. K. Rao. Modular aspects of term graph rewriting. Theoretical Computer Science. To appear. Special issue on Rewriting Techniques and Applications conference RTA'96."},{"key":"25_CR64","doi-asserted-by":"crossref","unstructured":"M. K. Rao. Semi-completeness of hierarchical and super-hierarchical combinations of term rewriting systems. In Theory and Practice of Software Development, TAPSOFT'95, volume 915 of Lecture Notes in Computer Science, pages 379\u2013393. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59293-8_208"},{"issue":"4","key":"25_CR65","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1145\/322217.322229","volume":"27","author":"J.-C. Raoult","year":"1980","unstructured":"J.-C. Raoult and J. Vuillemin. Operational and semantic equivalence between recursive programs. J. of the Association for Computing Machinery, 27(4):772\u2013796, October 1980.","journal-title":"J. of the Association for Computing Machinery"},{"key":"25_CR66","volume-title":"Proceedings of the Conference on Logic Programming and Automated Reasoning (St. Petersburg, Russia), volume 624 of Lecture Notes in Artificial Lntelligence","author":"C. Ringeissen","year":"1992","unstructured":"C. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In A. Voronkov, editor, Proceedings of the Conference on Logic Programming and Automated Reasoning (St. Petersburg, Russia), volume 624 of Lecture Notes in Artificial Lntelligence, Berlin, July 1992. Springer-Verlag."},{"key":"25_CR67","unstructured":"N. Robertson and P. Seymour. Graph minors 23: Nash-williams' immersion conjecture. Preprint, March 1996."},{"key":"25_CR68","unstructured":"N. Robertson and P. D. Seymour. Graph minors IV. Tree-width and well-quasiordering. Submitted 1982; revised January 1986."},{"key":"25_CR69","doi-asserted-by":"crossref","unstructured":"F. Seynhaeve, M. Tommasi, and R. Treinen. Grid structures and undecidable constraint theories. In Bidoit and Dauchet [6], pages 357\u2013368.","DOI":"10.1007\/BFb0030610"},{"key":"25_CR70","doi-asserted-by":"crossref","unstructured":"G. S\u00e9nizergues. On the termination problem for one-rule semi-Thue system. In Ganzinger [26], pages 302\u2013316.","DOI":"10.1007\/3-540-61464-8_61"},{"key":"25_CR71","first-page":"406","volume-title":"Proceedings of the International Conference on Typed Lambda Calculi and Applications (Utrecht, The Netherlands), volume 664 of Lecture Notes in Computer Science","author":"M. Takahashi","year":"1993","unstructured":"M. Takahashi. \u03bb-calculi with conditional rules. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications (Utrecht, The Netherlands), volume 664 of Lecture Notes in Computer Science, pages 406\u2013417, Berlin, 1993. Springer-Verlag."},{"key":"25_CR72","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata theory on trres and partial orders. In Bidoit and Dauchet [6], pages 20\u201338.","DOI":"10.1007\/BFb0030586"},{"key":"25_CR73","unstructured":"S. Tison. Automates comme outil de d\u00e9cision dans les arbres. Dossier d'habilitation \u00e0 diriger des recherches, December 1990. In French."},{"key":"25_CR74","unstructured":"H. Touzet. Propri\u00e9t\u00e9s combinatoires pour la terminaison de syst\u00e8mes de r\u00e9\u00e9criture. PhD thesis, Universit\u00e9 Henri Poincar\u00e9 \u2014Nancy 1, Nancy, France, September 1991. In French."},{"issue":"1","key":"25_CR75","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. J. of the Association for Computing Machinery, 34(1):128\u2013143, January 1987.","journal-title":"J. of the Association for Computing Machinery"},{"key":"25_CR76","unstructured":"Y. Toyama. Commutativity of term rewriting systems. In K. Fuchi and L. Kott, editors, Programming of Future Generation Computers II, pages 393\u2013407. North-Holland, 1988."},{"key":"25_CR77","doi-asserted-by":"crossref","unstructured":"Y. Toyama and M. Oyamaguchi. Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In N. Dershowitz and N. Lindenstrauss, editors, Workshop on Conditional Term Rewriting Systems (Jerusalem, July 1994), Lecture Notes in Computer Science. Springer-Verlag, to appear.","DOI":"10.1007\/3-540-60381-6_19"},{"key":"25_CR78","doi-asserted-by":"crossref","unstructured":"R. Treinen. The first-order theory of one-step rewriting is undecidable. In Ganzinger [26], pages 276\u2013286.","DOI":"10.1007\/3-540-61464-8_59"},{"key":"25_CR79","first-page":"379","volume-title":"Third International Symposium on the Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science","author":"V. v. Oostrom","year":"1994","unstructured":"V. v. Oostrom and F. v. Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In A. Nerode and Y. V. Matiyasevich, editors, Third International Symposium on the Logical Foundations of Computer Science, volume 813 of Lecture Notes in Computer Science, pages 379\u2013392, St. Petersburg, Russia, July 1994. Springer-Verlag."},{"key":"25_CR80","unstructured":"R. M. Verma. Unique normal forms and confluence for rewrite systems. In Int'l Joint Conf. on Artificial Intelligence, pages 362\u2013368, 1995."},{"key":"25_CR81","unstructured":"R. M. Verma. Unicity and modularity of confluence for term rewriting systems. Technical report, University of Houston, 1996."},{"key":"25_CR82","doi-asserted-by":"crossref","unstructured":"R. M. Verma. Unique normal forms for nonlinear term rewriting systems: Root overlaps. In Symp. on Fundamentals of Computation Theory, volume 1279 of Lecture Notes in Computer Science, pages 452\u2013462. Springer-Verlag, September 1997.","DOI":"10.1007\/BFb0036206"},{"key":"25_CR83","first-page":"275","volume-title":"Lecture Notes in Computer Science","author":"S. Vorobyov","year":"1996","unstructured":"S. Vorobyov. An improved lower bound for the elementary theories of trees. In M. A. McRobbie and J. K. Slaney, editors, 13th International Conference on Automated Deduction, Lecture Notes in Computer Science, pages 275\u2013287, New Brunswick, NJ, july\/august 1996. Springer-Verlag."},{"key":"25_CR84","doi-asserted-by":"crossref","unstructured":"S. Vorobyov. The first-order theory of one step rewriting in linear noetheran systems is undecidable. In Comon [12], pages 254\u2013268.","DOI":"10.1007\/3-540-62950-5_76"},{"key":"25_CR85","unstructured":"A. Weiermann. Bounding derivation lengths with functions from the slow growing hierarchy. Preprint M\u00fcnster, 1993."},{"key":"25_CR86","first-page":"237","volume-title":"Proceedings of the First International Workshop on Word Equations and Related Topics (T\u00fcbingen), volume 572 of Lecture Notes in Computer Science","author":"C. Wrathall","year":"1990","unstructured":"C. Wrathall. Confluence of one-rule Thue systems. In Proceedings of the First International Workshop on Word Equations and Related Topics (T\u00fcbingen), volume 572 of Lecture Notes in Computer Science, pages 237\u2013246, Berlin, 1990. Springer-Verlag."},{"key":"25_CR87","unstructured":"H. Zantema. Total termination of term rewriting is undecidable. Technical Report UU-CS-1994-55, Utrecht University, December 1994."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:34:01Z","timestamp":1555655641000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052380"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":87,"URL":"https:\/\/doi.org\/10.1007\/bfb0052380","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}