{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:50:48Z","timestamp":1762458648399},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705888"},{"type":"electronic","value":"9783540705901"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70590-1_7","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"94-109","source":"Crossref","is-referenced-by-count":10,"title":["Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Falke","sequence":"first","affiliation":[]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1\u20132","key":"7_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. TCS\u00a0236(1\u20132), 133\u2013178 (2000)","journal-title":"TCS"},{"key":"7_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":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-71316-6_8","volume-title":"Programming Languages and Systems","author":"F. Blanqui","year":"2007","unstructured":"Blanqui, F., Hardin, T., Weis, P.: On the implementation of construction functions for non-free concrete data types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 95\u2013109. Springer, Heidelberg (2007)"},{"issue":"4","key":"7_CR4","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-005-9022-x","volume":"34","author":"E. Contejean","year":"2005","unstructured":"Contejean, E., March\u00e9, C., Tom\u00e1s, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. JAR\u00a034(4), 325\u2013363 (2005)","journal-title":"JAR"},{"key":"7_CR5","unstructured":"Falke, S., Kapur, D.: Dependency pairs for rewriting with built-in numbers and semantic data structures. Technical Report TR-CS-2007-21, Department of Computer Science, University of New Mexico (2007), \n                  \n                    http:\/\/www.cs.unm.edu\/research\/tech-reports\/"},{"key":"7_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-540-73595-3_32","volume-title":"Automated Deduction \u2013 CADE-21","author":"S. Falke","year":"2007","unstructured":"Falke, S., Kapur, D.: Dependency pairs for rewriting with non-free constructors. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 426\u2013442. Springer, Heidelberg (2007)"},{"key":"7_CR7","unstructured":"Falke, S., Kapur, D.: Operational termination of conditional rewriting with built-in numbers and semantic data structures. Technical Report TR-CS-2007-22, Department of Computer Science, University of New Mexico (2007), \n                  \n                    http:\/\/www.cs.unm.edu\/research\/tech-reports\/"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"7_CR9","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":"7_CR10","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":"7_CR11","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: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"7_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/11559306_12","volume-title":"Frontiers of Combining Systems","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 216\u2013231. Springer, Heidelberg (2005)"},{"issue":"3","key":"7_CR13","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. JAR\u00a037(3), 155\u2013203 (2006)","journal-title":"JAR"},{"key":"7_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-73595-3_33","volume-title":"Automated Deduction \u2013 CADE-21","author":"J. Giesl","year":"2007","unstructured":"Giesl, J., Thiemann, R., Swiderski, S., Schneider-Kamp, P.: Proving termination by bounded increase. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 443\u2013459. Springer, Heidelberg (2007)"},{"issue":"4","key":"7_CR15","first-page":"474","volume":"205","author":"N. Hirokawa","year":"2007","unstructured":"Hirokawa, N., Middeldorp, A.: Tyrolean termination tool: Techniques and features. IC\u00a0205(4), 474\u2013511 (2007)","journal-title":"IC"},{"key":"7_CR16","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":"7_CR17","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"},{"key":"7_CR18","unstructured":"Lankford, D.S.: On proving term rewriting systems are Noetherian. Memo MTP-3, Mathematics Department, Louisiana Tech University, Ruston (1979)"},{"issue":"3","key":"7_CR19","first-page":"253","volume":"21","author":"C. March\u00e9","year":"1996","unstructured":"March\u00e9, C.: Normalized rewriting: An alternative to rewriting modulo a set of equations. JSC\u00a021(3), 253\u2013288 (1996)","journal-title":"JSC"},{"issue":"1","key":"7_CR20","first-page":"873","volume":"38","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Urbain, X.: Modular and incremental proofs of AC-termination. JSC\u00a038(1), 873\u2013897 (2004)","journal-title":"JSC"},{"issue":"2","key":"7_CR21","first-page":"233","volume":"28","author":"G.E. Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J.\u00a0ACM\u00a028(2), 233\u2013264 (1981)","journal-title":"J.\u00a0ACM"},{"key":"7_CR22","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du Premier Congr\u00e8s de Math\u00e9maticiens des Pays Slaves, pp. 92\u2013101 (1929)"},{"key":"7_CR23","unstructured":"Steinbach, J., K\u00fchler, U.: Check your ordering\u2014termination proofs and open problems. Technical Report SR-90-25, Universit\u00e4t Karlsruhe (1990)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:23:56Z","timestamp":1620015836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705888","9783540705901"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}