{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:09Z","timestamp":1725490869298},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_32","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"426-442","source":"Crossref","is-referenced-by-count":3,"title":["Dependency Pairs for Rewriting with Non-free Constructors"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Falke","sequence":"first","affiliation":[]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"32_CR1","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236(1-2), 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"32_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, Cambridge (1998)"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"2003","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 76\u201387. Springer, Heidelberg (2003)"},{"key":"32_CR4","unstructured":"Falke, S.: Automated termination analysis for equational rewriting. Diplomarbeit, Department of Computer Science, RWTH Aachen University, Germany (2004)"},{"key":"32_CR5","unstructured":"Falke, S., Kapur, D.: Dependency pairs for rewriting with non-free constructors. Technical Report TR-CS-2007-07, Department of Computer Science, University of New Mexico (2007), Available at http:\/\/www.cs.unm.edu\/research\/"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/3-540-45127-7_9","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 93\u2013108. Springer, Heidelberg (2001)"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Giesl, J., Kapur, D. (ed.): Journal of Automated Reasoning, 34(2), 34(4) & 37(3), 2005-2006. Special issues on Techniques for Automated Termination Proofs","DOI":"10.1007\/s10817-006-9052-z"},{"key":"32_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"32_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"issue":"3","key":"32_CR10","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning\u00a037(3), 155\u2013203 (2006)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"32_CR11","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1016\/j.ic.2006.08.010","volume":"205","author":"N. Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. Information and Computation\u00a0205(4), 474\u2013511 (2007)","journal-title":"Information and Computation"},{"key":"32_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-46508-1_3","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D. Kapur","year":"2000","unstructured":"Kapur, D., Sivakumar, G.: Proving associative-commutative termination using RPO-compatible orderings. In: Caferra, R., Salzer, G. (eds.) Automated Deduction in Classical and Non-Classical Logics. LNCS (LNAI), vol.\u00a01761, pp. 40\u201362. Springer, Heidelberg (2000)"},{"issue":"2","key":"32_CR13","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (RRL). Computers & Mathematics with Applications\u00a029(2), 91\u2013114 (1995)","journal-title":"Computers & Mathematics with Applications"},{"issue":"2","key":"32_CR14","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1017\/S0956796800003907","volume":"11","author":"H. Kirchner","year":"2001","unstructured":"Kirchner, H., Moreau, P.-E.: Promoting rewriting to a programming language. Journal of Functional Programming\u00a011(2), 207\u2013251 (2001)","journal-title":"Journal of Functional Programming"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10704567_3","volume-title":"Principles and Practice of Declarative Programming","author":"K. Kusakari","year":"1999","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol.\u00a01702, pp. 47\u201361. Springer, Heidelberg (1999)"},{"issue":"5","key":"32_CR16","first-page":"604","volume":"E84-D","author":"K. Kusakari","year":"2001","unstructured":"Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Transactions on Information and Systems\u00a0E84-D(5), 604\u2013612 (2001)","journal-title":"IEICE Transactions on Information and Systems"},{"issue":"3","key":"32_CR17","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1006\/jsco.1996.0011","volume":"21","author":"C. March\u00e9","year":"1996","unstructured":"March\u00e9, C.: Normalized rewriting: An alternative to rewriting modulo a set of equations. Journal of Symbolic Computation\u00a021(3), 253\u2013288 (1996)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"32_CR18","doi-asserted-by":"publisher","first-page":"873","DOI":"10.1016\/j.jsc.2004.02.003","volume":"38","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Urbain, X.: Modular and incremental proofs of AC-termination. Journal of Symbolic Computation\u00a038(1), 873\u2013897 (2004)","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"32_CR19","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G.E. Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. Journal of the ACM\u00a028(2), 233\u2013264 (1981)","journal-title":"Journal of the ACM"},{"issue":"2","key":"32_CR20","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1006\/inco.2002.3158","volume":"178","author":"A. Rubio","year":"2002","unstructured":"Rubio, A.: A fully syntactic AC-RPO. Information and Computation\u00a0178(2), 515\u2013533 (2002)","journal-title":"Information and Computation"},{"key":"32_CR21","unstructured":"Stein, C.: Das Dependency Pair Framework zur automatischen Terminierungsanalyse von Termersetzung modulo Gleichungen. Diplomarbeit, Department of Computer Science, RWTH Aachen University, Germany (in German) (2006)"},{"key":"32_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-540-25984-8_4","volume-title":"Automated Reasoning","author":"R. Thiemann","year":"2004","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 75\u201390. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:22Z","timestamp":1605762982000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}