{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:12:31Z","timestamp":1743052351837,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_29","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"384-399","source":"Crossref","is-referenced-by-count":5,"title":["On Transfinite Knuth-Bendix Orders"],"prefix":"10.1007","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[]},{"given":"Georg","family":"Moser","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"29_CR1","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B. Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. J. of Automated Reasoning\u00a044(3), 175\u2013205 (2010)","journal-title":"J. of Automated Reasoning"},{"key":"29_CR2","doi-asserted-by":"publisher","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":"29_CR3","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite Systems, pp. 245\u2013319 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Gaillourdet, J.-M., Hillenbrand, T., L\u00f6chner, B., Spies, H.: The New Waldmeister Loop at Work. In: Proc. of CADE, pp. 317\u2013321 (2003)","DOI":"10.1007\/978-3-540-45085-6_27"},{"key":"29_CR5","volume-title":"Set Theory","author":"T. Jech","year":"2002","unstructured":"Jech, T.: Set Theory. Springer, Heidelberg (2002)"},{"key":"29_CR6","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1112\/blms\/14.4.285","volume":"4","author":"L. Kirby","year":"1982","unstructured":"Kirby, L., Paris, J.: Accessible Independence Results for Peano Arithmetic. Bulletin London Mathematical Society\u00a04, 285\u2013293 (1982)","journal-title":"Bulletin London Mathematical Society"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Korovin, K., Voronkov, A.: Orienting Equalities with the Knuth-Bendix Order. In: Proc. of LICS, pp. 75\u201384 (2003)","DOI":"10.1109\/LICS.2003.1210047"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Kovacs","year":"2009","unstructured":"Kovacs, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, Springer, Heidelberg (2009)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 199\u2013213. Springer, Heidelberg (2009)"},{"issue":"4","key":"29_CR10","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. J. of Automated Reasoning\u00a036(4), 289\u2013310 (2006)","journal-title":"J. of Automated Reasoning"},{"key":"29_CR11","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)"},{"key":"29_CR12","unstructured":"McCune, B.: Private Communication (September 2004)"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: OTTER 3.0 Reference Manual and Guide. Technical Report ANL-94\/6, Argonne National Laboratory (January 1994)","DOI":"10.2172\/10129052"},{"issue":"2","key":"29_CR14","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00200-009-0094-4","volume":"20","author":"G. Moser","year":"2009","unstructured":"Moser, G.: The Hydra Battle and Cichon\u2019s Principle. AAECC\u00a020(2), 133\u2013158 (2009)","journal-title":"AAECC"},{"issue":"2-3","key":"29_CR15","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Schulz, S.: System Description: E\u00a00.81. In: Proc. of IJCAR, pp. 223\u2013228 (2004)","DOI":"10.1007\/978-3-540-25984-8_15"},{"issue":"3","key":"29_CR17","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1023\/A:1006393501098","volume":"24","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: The CADE-16 ATP System Competition. J. of Automated Reasoning\u00a024(3), 371\u2013396 (2000)","journal-title":"J. of Automated Reasoning"},{"issue":"4","key":"29_CR18","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. The FOF and CNF Parts, v3.5.0. J. of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. of Automated Reasoning"},{"key":"29_CR19","unstructured":"Vampire\u2019s homepage, http:\/\/www.vprover.org\/"},{"key":"29_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"issue":"1","key":"29_CR21","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1142\/S0218213006002540","volume":"15","author":"L. Wos","year":"2006","unstructured":"Wos, L.: Milestones for Automated Reasoning with Otter. Int. J. on Artificial Intelligence Tools\u00a015(1), 3\u201320 (2006)","journal-title":"Int. J. on Artificial Intelligence Tools"},{"issue":"2","key":"29_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","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T23:19:38Z","timestamp":1560381578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}