{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:38:36Z","timestamp":1725489516341},"publisher-location":"Berlin, Heidelberg","reference-count":57,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540731467"},{"type":"electronic","value":"9783540731474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73147-4_3","type":"book-chapter","created":{"date-parts":[[2007,8,17]],"date-time":"2007-08-17T04:01:50Z","timestamp":1187323310000},"page":"44-67","source":"Crossref","is-referenced-by-count":4,"title":["Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations"],"prefix":"10.1007","author":[{"given":"Isabelle","family":"Gnaedig","sequence":"first","affiliation":[]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-62950-5_68","volume-title":"Rewriting Techniques and Applications","author":"T. Arts","year":"1997","unstructured":"Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Comon, H. (ed.) Rewriting Techniques and Applications. LNCS, vol.\u00a01232, pp. 157\u2013171. Springer, Heidelberg (1997)"},{"key":"3_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and all That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, New York, NY, USA (1998)"},{"key":"3_CR3","unstructured":"Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom Manual LORIA, Nancy (France) (version 2.4 edn.) (2006)"},{"key":"3_CR4","unstructured":"Bezem, M., Klop, J.W., de Vrijer, R.: Term Rewriting Systems. In: Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)"},{"key":"3_CR5","unstructured":"Bouhoula, A., Jaquemard, F.: Automatic verification of. sufficient completeness for. specifications of complex data structures. Technical Report RR-LSV-05-17, INRIA (2005)"},{"issue":"1-2","key":"3_CR6","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/S0304-3975(96)80708-0","volume":"170","author":"A. Bouhoula","year":"1996","unstructured":"Bouhoula, A.: Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science\u00a0170(1-2), 245\u2013276 (1996)","journal-title":"Theoretical Computer Science"},{"key":"3_CR7","unstructured":"Bouhoula, A., Jacquemard, F.: Automating sufficient completeness check for conditional and constrained TRS. In: Levy, J (ed): Proceedings of the 20th International Workshop on Unification (UNIF 2006), Seattle, Washington, USA (August 2006)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/3-540-56868-9_25","volume-title":"Rewriting Techniques and Applications","author":"A.-C. Caron","year":"1993","unstructured":"Caron, A-C., Coquide, J-L., Dauchet, M.: Encompassment properties and automata with constraints. In: Kirchner, C. (ed.) Rewriting Techniques and Applications. LNCS, vol.\u00a0690, pp. 328\u2013342. Springer, Heidelberg (1993)"},{"key":"3_CR9","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus \u2014 Part\u00a0I and II. Logic Journal of the Interest Group in Pure and Applied Logics\u00a09, 427\u2013498 (2001)","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"3_CR10","volume-title":"Electronic Notes in Theoretical Computer Science","author":"H. Cirstea","year":"2003","unstructured":"Cirstea, H., Kirchner, C., Liquori, L., Wack, B.: Rewrite strategies in the rewriting calculus. In: Gramlich, B., Lucas, S. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a086, Elsevier, North-Holland, Amsterdam (2003)"},{"issue":"2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theoretical Computer Science\u00a0285(2), 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/3-540-16780-3_85","volume-title":"CADE 1986","author":"H. Comon","year":"1986","unstructured":"Comon, H.: Sufficient completeness, term rewriting system and anti-unification. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 128\u2013140. Springer, Heidelberg (1986)"},{"key":"3_CR13","first-page":"26","volume-title":"Ground reducibility is EXPTIME-complete","author":"H. Comon","year":"1997","unstructured":"Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. In: Proc. 12th IEEE Symp. Logic in Computer Science, pp. 26\u201334. IEEE Comp. Soc. Press, Washington, DC, USA (1997)"},{"key":"3_CR14","first-page":"244","volume-title":"Rewrite Systems","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Handbook of Theoretical Computer Science (Also as: Research report 478, LRI). In: Rewrite Systems, vol.\u00a0B, pp. 244\u2013320. Elsevier Science Publishers, B. V. North-Holland (1990)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1016\/B978-044450813-3\/50011-4","volume-title":"Handbook of Automated Reasoning","author":"N. Dershowitz","year":"2001","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, pp. 535\u2013610. Elsevier Science, Amsterdam (2001)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-540-32033-3_3","volume-title":"RTA","author":"M.-L. Fern\u00e1ndez","year":"2005","unstructured":"Fern\u00e1ndez, M.-L., Godoy, G., Rubio, A.: Orderings for innermost termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 17\u201331. Springer, Heidelberg (2005)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Termination of rewriting with local strategies. In: Bonacina, M.P., Gramlich, B. (eds.) Selected papers of the 4th International Workshop on Strategies in Automated. Deduction. Electronic Notes in Theoretical Computer Science, vol.\u00a058, Elsevier Science Publishers, B. V. North-Holland (2001)","DOI":"10.1016\/S1571-0661(04)00284-1"},{"key":"3_CR18","volume-title":"Proceedings of the 4th International Conference on Principles and Practice of Declarative Programming","author":"O. Fissore","year":"2002","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Cariboo: An induction based proof tool for termination with strategies. In: Fissore, O., Gnaedig, I., Kirchner, H. (eds.) Proceedings of the 4th International Conference on Principles and Practice of Declarative Programming, Pittsburgh (USA), ACM Press, New York (2002)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Outermost ground termination. In: Proceedings of the 4th International Workshop on Rewriting Logic and Its Applications, Pisa, Italy, September 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a071, Elsevier Science Publishers B. V (North-Holland), Amsterdam (2002)","DOI":"10.1016\/S1571-0661(05)82535-6"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","first-page":"356","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"O. Fissore","year":"2004","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: A proof of weak termination providing the right way to terminate. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 356\u2013371. Springer, Heidelberg (2004)"},{"key":"3_CR21","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H., Moussa, L.: Cariboo, a termination proof tool for rewriting-based programming languages with strategies, Version 1.1. Free GPL Licence, APP registration IDDN.FR.001.170013.001.S.P.2005.000.10600 (December 2005), Available at http:\/\/protheo.loria.fr\/softwares\/cariboo\/"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/3-540-48685-2_23","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"1999","unstructured":"Giesl, J., Middeldorp, A.: Transforming Context-Sensitive Rewrite Systems. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 271\u2013285. Springer, Heidelberg (1999)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/3-540-45005-X_20","volume-title":"(DLT 2002)","author":"J. Giesl","year":"2003","unstructured":"Giesl, J., Middeldorp, A.: Innermost termination of context-sensitive rewriting. In: Ito, M., Toyama, M. (eds.) DLT 2002. LNCS, vol.\u00a02450, pp. 231\u2013244. Springer, Heidelberg (2003)"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","first-page":"165","volume-title":"LPAR \u201903","author":"J. Giesl","year":"2003","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 165\u2013179. Springer, Heidelberg (2003)"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/11805618_23","volume-title":"RTA","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated Termination Analysis for Haskell: From term rewriting to programming languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 297\u2013312. Springer, Heidelberg (2006)"},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/1140335.1140351","volume-title":"Proceedings of the Eighth ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming","author":"I. Gnaedig","year":"2006","unstructured":"Gnaedig, I., Kirchner, H.: Computing constructor forms with non terminating rewrite programs. In: Maher, M. (ed.) Proceedings of the Eighth ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, Venice, Italy, pp. 121\u2013132. ACM Press, New York (July 2006)"},{"key":"3_CR27","unstructured":"Gnaedig, I., Kirchner, H.: Termination of rewriting under strategies: a generic approach, Submitted. Also as HAL-INRIA Open Archive Number inria-00113156 (2006)"},{"key":"3_CR28","unstructured":"Gnaedig, I., Kirchner, H., Genet, T.: Induction for Termination. Technical Report 99.R.338, LORIA, Nancy (France) (December 1999)"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BFb0015747","volume-title":"Automata, Languages and Programming","author":"J.A. Goguen","year":"1985","unstructured":"Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Operational semantics for order-sorted algebra. In: Brauer, W. (ed.) Automata, Languages and Programming. LNCS, vol.\u00a0194, pp. 221\u2013231. Springer, Heidelberg (1985)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"J. Goubault- Larrecq","year":"1998","unstructured":"Goubault- Larrecq, J.: A proof of weak termination of typed lambda-sigma-calculi. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, Springer, Heidelberg (1998)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BFb0013069","volume-title":"Logic Programming and Automated Reasoning","author":"B. Gramlich","year":"1992","unstructured":"Gramlich, B.: Relating innermost, weak, uniform and modular termination of term rewriting systems. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 285\u2013296. Springer, Heidelberg (1992)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-61464-8_45","volume-title":"Rewriting Techniques and Applications","author":"B. Gramlich","year":"1996","unstructured":"Gramlich, B.: On proving termination by innermost termination. In: Ganzinger, H. (ed.) Rewriting Techniques and Applications. LNCS, vol.\u00a01103, pp. 93\u2013107. Springer, Heidelberg (1996)"},{"issue":"1","key":"3_CR33","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(96)00042-4","volume":"165","author":"B. Gramlich","year":"1996","unstructured":"Gramlich, B.: On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems. Theoretical Computer Science\u00a0165(1), 97\u2013131 (1996)","journal-title":"Theoretical Computer Science"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-540-32033-3_13","volume-title":"RTA 2005","author":"J. Hendrix","year":"2005","unstructured":"Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 165\u2013174. Springer, Heidelberg (2005)"},{"issue":"2","key":"3_CR35","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G., Hullot, J.-M.: Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2) , 239\u2013266 (1982), In: Preliminary version Proceedings 21st Symposium on Foundations of Computer Science, October 1982, IEEE (1980)","journal-title":"Journal of Computer and System Sciences"},{"key":"3_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(89)90062-X","volume":"82","author":"J.-P. Jouannaud","year":"1989","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in theories without constructors. Information and Computation\u00a082, 1\u201333 (1989)","journal-title":"Information and Computation"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/3-540-16780-3_83","volume-title":"8th International Conference on Automated Deduction","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Proof by induction using test sets. In: Siekmann, J.H. (ed.) 8th International Conference on Automated Deduction. LNCS, vol.\u00a0230, pp. 99\u2013117. Springer, Heidelberg (1986)"},{"key":"3_CR38","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient completeness and related properties of term rewriting systems. Acta Informatica\u00a024, 395\u2013415 (1987)","journal-title":"Acta Informatica"},{"issue":"3","key":"3_CR39","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue d\u2019Intelligence Artificielle. Special issue on Automatic Deduction\u00a04(3), 9\u201352 (1990)","journal-title":"Special issue on Automatic Deduction"},{"key":"3_CR40","series-title":"ch. 8","first-page":"131","volume-title":"Principles and Practice of Constraint Programming. The Newport Papers.","author":"C. Kirchner","year":"1995","unstructured":"Kirchner, C., Kirchner, H., Vittek, M.: Designing constraint logic programming languages using computational systems. In: Van Hentenryck, P., Saraswat, V. (eds.) Principles and Practice of Constraint Programming. The Newport Papers. ch. 8, pp. 131\u2013158. The MIT press, Cambridge, MA (1995)"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","first-page":"348","volume-title":"EUROCAL \u201985","author":"E. Kounalis","year":"1985","unstructured":"Kounalis, E.: Completeness in data type specifications. In: Caviness, B.F. (ed.) ISSAC 1985 and EUROCAL 1985. LNCS, vol.\u00a0204, pp. 348\u2013362. Springer, Heidelberg (1985)"},{"key":"3_CR42","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0304-3975(92)90279-O","volume":"106","author":"E. Kounalis","year":"1992","unstructured":"Kounalis, E.: Testing for the ground (co-)reducibility property in term-rewriting systems. Theoretical Computer Science\u00a0106, 87\u2013117 (1992)","journal-title":"Theoretical Computer Science"},{"key":"3_CR43","doi-asserted-by":"publisher","first-page":"210","DOI":"10.2307\/1993287","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"Kruskal, J.B.: Well-quasi ordering, the tree theorem and Vazsonyi\u2019s conjecture. Trans. Amer. Math. Soc.\u00a095, 210\u2013225 (1960)","journal-title":"Trans. Amer. Math. Soc."},{"issue":"1","key":"3_CR44","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0890-5401(90)90033-E","volume":"84","author":"A. Lazrek","year":"1990","unstructured":"Lazrek, A., Lescanne, P., Thiel, J.-J.: Tools for proving inductive equalities, relative completeness and \u03c9-completeness. Information and Computation\u00a084(1), 47\u201370 (1990)","journal-title":"Information and Computation"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-61440-0_122","volume-title":"Automata, Languages and Programming","author":"S. Lucas","year":"1996","unstructured":"Lucas, S.: Termination of context-sensitive rewriting by rewriting. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol.\u00a01099, pp. 122\u2013133. Springer, Heidelberg (1996)"},{"key":"3_CR46","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/773184.773194","volume-title":"PPDP 2001","author":"S. Lucas","year":"2001","unstructured":"Lucas, S.: Termination of on-demand rewriting and termination of OBJ programs. In: Sondergaard, H. (ed.) PPDP 2001. Proc. of 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Firenze, Italy, pp. 82\u201393. ACM Press, New York (2001)"},{"key":"3_CR47","series-title":"Lecture Notes in Artificial Intelligence","first-page":"669","volume-title":"LPAR\u201901","author":"S. Lucas","year":"2001","unstructured":"Lucas, S.: Termination of rewriting with strategy annotations. In: Voronkov, A., Nieuwenhuis, R. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 669\u2013684. Springer, Heidelberg (2001)"},{"issue":"1","key":"3_CR48","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1016\/S0890-5401(02)93176-7","volume":"178","author":"S. Lucas","year":"2002","unstructured":"Lucas, S.: Context-sensitive rewriting strategies. Information and Computation\u00a0178(1), 294\u2013343 (2002)","journal-title":"Information and Computation"},{"issue":"2","key":"3_CR49","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0304-3975(01)00356-5","volume":"285","author":"N. Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic and its applications: Preface. Theoretical Computer Science\u00a0285(2), 119\u2013120 (2002)","journal-title":"Theoretical Computer Science"},{"key":"3_CR50","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"153","volume-title":"WRLA 2004","author":"J. Meseguer","year":"2004","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. In: Marti-Oliet, N., Thati, P., Mart\u00ed-Oliet, N. (eds.) WRLA 2004. Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science, vol.\u00a0117, pp. 153\u2013182. 1, 1 (2004)"},{"issue":"3 & 4","key":"3_CR51","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF01190830","volume":"5","author":"A. Middeldorp","year":"1994","unstructured":"Middeldorp, A., Hamoen, E.: Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computation\u00a05(3 & 4), 213\u2013253 (1994)","journal-title":"Applicable Algebra in Engineering, Communication and Computation"},{"key":"3_CR52","series-title":"Lecture Notes in Computer Science","first-page":"61","volume-title":"CC\u20192003","author":"P.-E. Moreau","year":"2003","unstructured":"Moreau, P.-E., Ringeissen, C., Vittek, M.: A pattern matching compiler for multiple target languages. In: Hedin, G. (ed.) CC 2003 and ETAPS 2003. LNCS, vol.\u00a02622, pp. 61\u201376. Springer, Heidelberg (2003)"},{"key":"3_CR53","volume-title":"WRS 2001","author":"Q.-H. Nguyen","year":"2001","unstructured":"Nguyen, Q-H.: Compact normalisation trace via lazy rewriting. In: Lucas, S., Gramlich, B. (eds.) WRS 2001. Proc. 1st International Workshop on Reduction Strategies in Rewriting and Programming, vol.\u00a057, Elsevier Science Publishers B. V., North-Holland, Amsterdam (2001)"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","first-page":"257","volume-title":"Theoretical Computer Science","author":"T. Nipkow","year":"1983","unstructured":"Nipkow, T., Weikum, G.: A decidability result about sufficient completeness of axiomatically specified abstract data types. In: Cremers, A.B., Kriegel, H.-P. (eds.) Theoretical Computer Science. LNCS, vol.\u00a0145, pp. 257\u2013268. Springer, Heidelberg (1983)"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BFb0032752","volume-title":"Static Analysis Symposium\u201997","author":"S.E. Panitz","year":"1997","unstructured":"Panitz, S.E., Schmidt-Schauss, M.: TEA: Automatically proving termination of programs in a non-strict higher-order functional language. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, pp. 345\u2013360. Springer, Heidelberg (1997)"},{"key":"3_CR56","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"Plaisted, D.: Semantic confluence tests and completion methods. Information and Control\u00a065, 182\u2013215 (1985)","journal-title":"Information and Control"},{"key":"3_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-45127-7_27","volume-title":"Rewriting Techniques and Applications (RTA\u201901)","author":"E. Visser","year":"2001","unstructured":"Visser, E.: Stratego: A language for program transformation based on rewriting strategies. System description of Stratego 0.5 (LP:0). In: Middeldorp, A. (ed.) Rewriting Techniques and Applications 2001. LNCS, vol.\u00a02051, pp. 357\u2013361. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Rewriting, Computation and Proof"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73147-4_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T23:15:07Z","timestamp":1629587707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73147-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540731467","9783540731474"],"references-count":57,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73147-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}