{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:41:53Z","timestamp":1742964113145,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_10","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"152-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion"],"prefix":"10.1007","author":[{"given":"Haruhiko","family":"Sato","sequence":"first","affiliation":[]},{"given":"Sarah","family":"Winkler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"10_CR1","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":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"2\u20133","key":"10_CR3","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2\u20133), 195\u2013220 (2008)","journal-title":"JAR"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","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. 3452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"10_CR5","unstructured":"Klein, D., Hirokawa, N.: Maximal completion. In: RTA, vol. 10 of LIPIcs, pp. 71\u201380 (2011)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen \u2013 a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239\u2013270. Springer, Heidelberg (2013)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Sato, H., Winkler, S.: A satisfiability encoding of dependency pair techniques for maximal completion. In: WST (2014)","DOI":"10.1007\/978-3-319-21401-6_10"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-74621-8_18","volume-title":"Frontiers of Combining Systems","author":"P Schneider-Kamp","year":"2007","unstructured":"Schneider-Kamp, P., Thiemann, R., Annov, E., Codish, M., Giesl, J.: Proving termination using recursive path orders and SAT solving. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 267\u2013282. Springer, Heidelberg (2007)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-642-31365-3_41","volume-title":"Automated Reasoning","author":"T Sternagel","year":"2012","unstructured":"Sternagel, T., Zankl, H.: KBCV \u2013 Knuth-Bendix Completion Visualizer. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 530\u2013536. Springer, Heidelberg (2012)"},{"issue":"5","key":"10_CR10","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.ipl.2006.01.009","volume":"98","author":"A Stump","year":"2006","unstructured":"Stump, A., L\u00f6chner, B.: Knuth-Bendix completion of theories of commuting group endomorphisms. IPL 98(5), 195\u2013198 (2006)","journal-title":"IPL"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11805618_22","volume-title":"Term Rewriting and Applications","author":"I Wehrman","year":"2006","unstructured":"Wehrman, I., Stump, A., Westbrook, E.: Slothrop: knuth-bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 287\u2013296. Springer, Heidelberg (2006)"},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10817-012-9249-2","volume":"50","author":"S Winkler","year":"2013","unstructured":"Winkler, S., Sato, H., Middeldorp, A., Kurihara, M.: Multi-completion with termination tools. JAR 50(3), 317\u2013354 (2013)","journal-title":"JAR"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Science of Computer Programming (2014). doi:10.1016\/j.scico.2014.07.009","DOI":"10.1016\/j.scico.2014.07.009"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-540-69507-3_50","volume-title":"SOFSEM 2007: Theory and Practice of Computer Science","author":"H Zankl","year":"2007","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: Constraints for argument filterings. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Pl\u00e1\u0161il, F. (eds.) SOFSEM 2007. LNCS, vol. 4362, pp. 579\u2013590. Springer, Heidelberg (2007)"},{"issue":"2","key":"10_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-009-9131-z","volume":"43","author":"H Zankl","year":"2009","unstructured":"Zankl, H., Hirokawa, N., Middeldorp, A.: KBO orientability. JAR 43(2), 173\u2013201 (2009)","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T14:08:36Z","timestamp":1675865316000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}