{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:20Z","timestamp":1740099140758,"version":"3.37.3"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319964171"},{"type":"electronic","value":"9783319964188"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96418-8_29","type":"book-chapter","created":{"date-parts":[[2018,7,13]],"date-time":"2018-07-13T06:57:13Z","timestamp":1531465033000},"page":"245-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards a Unified Ordering for Superposition-Based Automated Reasoning"],"prefix":"10.1007","author":[{"given":"Jan","family":"Jakub\u016fv","sequence":"first","affiliation":[]},{"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,14]]},"reference":[{"key":"29_CR1","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"\u0141 Czajka","year":"2018","unstructured":"Czajka, \u0141., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61, 423\u2013453 (2018)","journal-title":"J. Autom. Reason."},{"key":"29_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"issue":"4","key":"29_CR3","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. Autom. Reason. 36(4), 289\u2013310 (2006)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"29_CR4","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1142\/S0218213006002564","volume":"15","author":"B L\u00f6chner","year":"2006","unstructured":"L\u00f6chner, B.: Things to know when implementing LPO. Int. J. Artif. Intell. Tools 15(1), 53\u201380 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"issue":"3","key":"29_CR5","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. J. Autom. Reason. 19(3), 263\u2013276 (1997)","journal-title":"J. Autom. Reason."},{"key":"29_CR6","unstructured":"Middeldorp, A.: Term rewriting lecture notes. In: 9th International School on Rewriting (ISR 2017) (2017)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"issue":"4","key":"29_CR8","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. from CNF to TH0, TPTP v6.4.0. J. Automa. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Automa. Reason."},{"issue":"5","key":"29_CR9","doi-asserted-by":"publisher","first-page":"607","DOI":"10.3233\/AIC-160709","volume":"29","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun. 29(5), 607\u2013619 (2016)","journal-title":"AI Commun."},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Unifying the Knuth-Bendix, recursive path and polynomial orders. In: PPDP, pp. 181\u2013192. ACM (2013)","DOI":"10.1145\/2505879.2505885"},{"key":"29_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.scico.2014.07.009","volume":"111","author":"A Yamada","year":"2015","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: A unified ordering for termination proving. Sci. Comput. Program. 111, 110\u2013134 (2015)","journal-title":"Sci. Comput. Program."}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2018"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96418-8_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,13]],"date-time":"2018-07-13T07:10:47Z","timestamp":1531465847000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96418-8_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319964171","9783319964188"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96418-8_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}