{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:20:03Z","timestamp":1781076003307,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540405597","type":"print"},{"value":"9783540450856","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_5","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"47-59","source":"Crossref","is-referenced-by-count":5,"title":["An AC-Compatible Knuth-Bendix Order"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_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)"},{"issue":"1","key":"5_CR2","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/0020-0190(92)90024-P","volume":"43","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L.: Associative-commutative reduction orderings. Information Processing Letters\u00a043(1), 21\u201327 (1992)","journal-title":"Information Processing Letters"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-15976-2_11","volume-title":"Rewriting Techniques and Applications","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., Plaisted, D.: Associative path orderings. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol.\u00a0202, pp. 241\u2013254. Springer, Heidelberg (1985)"},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A.B. Cherifa","year":"1987","unstructured":"Cherifa, A.B., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming\u00a09(2), 137\u2013159 (1987)","journal-title":"Science of Computer Programming"},{"key":"5_CR5","unstructured":"Dershowitz, N., Hsiang, J., Josephson, A., Plaisted, D.: Associative-commutative rewriting. In: Proc. International Joint Conference on Artificial Intelligence (IJCAI), pp. 940\u2013944 (1983)"},{"issue":"8","key":"5_CR6","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM (CACM)\u00a022(8), 465\u2013476 (1979)","journal-title":"Communications of the ACM (CACM)"},{"issue":"2","key":"5_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF01237233","volume":"28","author":"J. Dick","year":"1990","unstructured":"Dick, J., Kalmus, J., Martin, U.: Automating the Knuth-Bendix ordering. Acta Informatica\u00a028(2), 95\u2013119 (1990)","journal-title":"Acta Informatica"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-16780-3_79","volume-title":"8th International Conference on Automated Deduction","author":"I. Gnaedig","year":"1986","unstructured":"Gnaedig, I., Lescanne, P.: Proving termination of associative commutative rewriting systems by rewriting. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 52\u201361. Springer, Heidelberg (1986)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-62950-5_67","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1997","unstructured":"Kapur, D., Sivakumar, G.: A total, ground path ordering for proving termination of ac-rewrite systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 142\u2013156. Springer, Heidelberg (1997)"},{"key":"5_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","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-communicative termination using rpo-compatible orderings. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 39\u201361. Springer, Heidelberg (2000)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-53487-3_40","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"D. Kapur","year":"1990","unstructured":"Kapur, D., Sivakumar, G., Zhang, H.: A new method for proving termination of ac-rewrite systems. In: Veni Madhavan, C.E., Nori, K.V. (eds.) FSTTCS 1990. LNCS, vol.\u00a0472, pp. 133\u2013148. Springer, Heidelberg (1990)"},{"issue":"2","key":"5_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BF00881859","volume":"14","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Sivakumar, G., Zhang, H.: A path ordering for proving termination of ac rewrite systems. Journal of Automated Reasoning\u00a014(2), 293\u2013316 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45127-7_12","volume-title":"Rewriting Techniques and Applications","author":"K. Korovin","year":"2001","unstructured":"Korovin, K., Voronkov, A.: Verifying orientability of rewrite rules using the Knuth-Bendix order. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 137\u2013153. Springer, Heidelberg (2001); full version to appear in Information and Computation"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: Orienting equalities using the Knuth\u2013Bendix order. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science, LICS 2003 (2003) (to appear)","DOI":"10.1109\/LICS.2003.1210047"},{"key":"5_CR15","unstructured":"March\u00e9, C.: Associative-commutative reduction orderings via head-preserving interpretations. Technical Report 95-2, E.N.S. de Cachan (1995)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-53904-2_115","volume-title":"Rewriting Techniques and Applications","author":"P. Narendran","year":"1991","unstructured":"Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. In: Book, R.V. (ed.) RTA 1991. LNCS, vol.\u00a0488, pp. 423\u2013434. Springer, Heidelberg (1991)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","first-page":"374","volume-title":"Rewriting Techniques and Applications","author":"R. Nieuwenhuis","year":"1993","unstructured":"Nieuwenhuis, R., Rubio, A.: A precedence-based total AC-compatible ordering. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 374\u2013388. Springer, Heidelberg (1993)"},{"key":"5_CR18","unstructured":"Rubio, A.: A fully syntactic AC-RPO. To appear in Information and Computation"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-48685-2_11","volume-title":"Rewriting Techniques and Applications","author":"A. Rubio","year":"1999","unstructured":"Rubio, A.: A fully syntactic AC-RPO. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 133\u2013147. Springer, Heidelberg (1999)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","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. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T21:56:51Z","timestamp":1553205411000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}