{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:17:38Z","timestamp":1725794258448},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319071503"},{"type":"electronic","value":"9783319071510"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07151-0_20","type":"book-chapter","created":{"date-parts":[[2014,5,21]],"date-time":"2014-05-21T23:30:14Z","timestamp":1400715014000},"page":"319-335","source":"Crossref","is-referenced-by-count":2,"title":["AC-KBO Revisited"],"prefix":"10.1007","author":[{"given":"Akihisa","family":"Yamada","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarah","family":"Winkler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nao","family":"Hirokawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-16310-4_4","volume-title":"Rewriting Logic and Its Applications","author":"B. Alarc\u00f3n","year":"2010","unstructured":"Alarc\u00f3n, B., Lucas, S., Meseguer, J.: A dependency pair framework for A\u2009\u2228\u2009C-termination. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 35\u201351. Springer, Heidelberg (2010)"},{"issue":"1-2","key":"20_CR2","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-2), 133\u2013178 (2000)","journal-title":"TCS"},{"key":"20_CR3","first-page":"329","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., Plaisted, D.A.: Termination orderings for associative-commutative rewriting systems. JSC\u00a01, 329\u2013349 (1985)","journal-title":"JSC"},{"issue":"2","key":"20_CR4","first-page":"137","volume":"9","author":"A. Ben Cherifa","year":"1987","unstructured":"Ben Cherifa, A., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. SCP\u00a09(2), 137\u2013159 (1987)","journal-title":"SCP"},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-010-9211-0","volume":"49","author":"M. Codish","year":"2012","unstructured":"Codish, M., Giesl, J., Schneider-Kamp, P., Thiemann, R.: SAT solving for termination proofs with recursive path orders and dependency pairs. JAR\u00a049(1), 53\u201393 (2012)","journal-title":"JAR"},{"issue":"3","key":"20_CR6","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. TCS\u00a017(3), 279\u2013301 (1982)","journal-title":"TCS"},{"key":"20_CR7","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\u2013107. Springer, Heidelberg (2001)"},{"key":"20_CR8","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, New York (1970)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: An AC-compatible Knuth-Bendix order. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol.\u00a02741, pp. 47\u201359. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45085-6_5"},{"issue":"2","key":"20_CR10","first-page":"165","volume":"183","author":"K. Korovin","year":"2003","unstructured":"Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order. I&C\u00a0183(2), 165\u2013186 (2003)","journal-title":"I&C"},{"key":"20_CR11","unstructured":"Kusakari, K.: AC-Termination and Dependency Pairs of Term Rewriting Systems. PhD thesis, JAIST (2000)"},{"issue":"5","key":"20_CR12","first-page":"439","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), 439\u2013447 (2001)","journal-title":"IEICE Transactions on Information and Systems"},{"issue":"4","key":"20_CR13","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/s10817-006-9031-4","volume":"36","author":"B. L\u00f6chner","year":"2006","unstructured":"L\u00f6chner, B.: Things to know when implementing KBO. JAR\u00a036(4), 289\u2013310 (2006)","journal-title":"JAR"},{"key":"20_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-75560-9_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Ludwig","year":"2007","unstructured":"Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 348\u2013362. Springer, Heidelberg (2007)"},{"issue":"1","key":"20_CR15","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":"20_CR16","first-page":"515","volume":"178","author":"A. Rubio","year":"2002","unstructured":"Rubio, A.: A fully syntactic AC-RPO. I&C\u00a0178(2), 515\u2013533 (2002)","journal-title":"I&C"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/3-540-53162-9_52","volume-title":"Algebraic and Logic Programming","author":"J. Steinbach","year":"1990","unstructured":"Steinbach, J.: AC-termination of rewrite systems: A modified Knuth-Bendix ordering. In: Kirchner, H., Wechler, W. (eds.) ALP 1990. LNCS, vol.\u00a0463, pp. 372\u2013386. Springer, Heidelberg (1990)"},{"key":"20_CR18","unstructured":"Thiemann, R., Allais, G., Nagele, J.: On the formalization of termination techniques based on multiset orderings. In: Proc. RTA-23. LIPIcs, vol.\u00a015, pp. 339\u2013354 (2012)"},{"key":"20_CR19","unstructured":"Winkler, S.: Termination Tools in Automated Reasoning. PhD thesis, UIBK (2013)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-642-28717-6_33","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Winkler","year":"2012","unstructured":"Winkler, S., Zankl, H., Middeldorp, A.: Ordinals and Knuth-Bendix orders. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 420\u2013434. Springer, Heidelberg (2012)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Yamada, A., Winkler, S., Hirokawa, N., Middeldorp, A.: AC-KBO revisited. CoRR abs\/1403.0406 (2014)","DOI":"10.1007\/978-3-319-07151-0_20"},{"issue":"2","key":"20_CR22","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\u00a043(2), 173\u2013201 (2009)","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07151-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T18:23:47Z","timestamp":1558895027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-07151-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319071503","9783319071510"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07151-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}