{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T16:27:24Z","timestamp":1726849644739},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319942049"},{"type":"electronic","value":"9783319942056"}],"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-94205-6_31","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:22:50Z","timestamp":1530274970000},"page":"472-480","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["M\u00e6dMax: A Maximal Ordered Completion Tool"],"prefix":"10.1007","author":[{"given":"Sarah","family":"Winkler","sequence":"first","affiliation":[]},{"given":"Georg","family":"Moser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"issue":"1\u20132","key":"31_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0747-7171(03)00024-5","volume":"36","author":"J Avenhaus","year":"2003","unstructured":"Avenhaus, J., Hillenbrand, T., L\u00f6chner, B.: On using ground joinable equations in equational theorem proving. JSC 36(1\u20132), 217\u2013233 (2003). \nhttps:\/\/doi.org\/10.1016\/S0747-7171(03)00024-5","journal-title":"JSC"},{"key":"31_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). \nhttps:\/\/doi.org\/10.1017\/CBO9781139172752"},{"key":"31_CR3","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures, Rewriting Techniques of Progress in Theoretical Computer Science","author":"L Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures, Rewriting Techniques of Progress in Theoretical Computer Science, vol. 2, pp. 1\u201330. Academic Press, Cambridge (1989)"},{"issue":"1","key":"31_CR4","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/601775.601777","volume":"4","author":"H Comon","year":"2003","unstructured":"Comon, H., Narendran, P., Nieuwenhuis, R., Rusinowitch, M.: Deciding the confluence of ordered term rewrite systems. ACM TOCL 4(1), 33\u201355 (2003). \nhttps:\/\/doi.org\/10.1145\/601775.601777","journal-title":"ACM TOCL"},{"key":"31_CR5","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). \nhttps:\/\/doi.org\/10.1007\/11817963_11"},{"key":"31_CR6","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A., Sternagel, C., Winkler, S.: Infinite runs in abstract completion. In: Proceedings of the 2nd FSCD. LIPIcs, vol. 84, pp. 19:1\u201319:16 (2017). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.19","DOI":"10.4230\/LIPIcs.FSCD.2017.19"},{"key":"31_CR7","doi-asserted-by":"publisher","unstructured":"Klein, D., Hirokawa, N.: Maximal completion. In: Proceedings of the 22nd RTA. LIPIcs, vol. 10, pp. 71\u201380 (2011). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.71","DOI":"10.4230\/LIPIcs.RTA.2011.71"},{"key":"31_CR8","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4","volume-title":"Computational Problems in Abstract Algebra","author":"DE Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970). \nhttps:\/\/doi.org\/10.1016\/B978-0-08-012975-4"},{"key":"31_CR9","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"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-52885-7_100","volume-title":"10th International Conference on Automated Deduction","author":"U Martin","year":"1990","unstructured":"Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 366\u2013380. Springer, Heidelberg (1990). \nhttps:\/\/doi.org\/10.1007\/3-540-52885-7_100"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-21401-6_10","volume-title":"Automated Deduction \u2013 CADE-25","author":"H Sato","year":"2015","unstructured":"Sato, H., Winkler, S.: Encoding dependency pair techniques and control strategies for maximal completion. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 152\u2013162. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_10"},{"issue":"e24","key":"31_CR12","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1017\/S0956796817000168","volume":"27","author":"P Schultz","year":"2017","unstructured":"Schultz, P., Wisnesky, R.: Algebraic data integration. JFP 27(e24), 51 (2017). \nhttps:\/\/doi.org\/10.1017\/S0956796817000168","journal-title":"JFP"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-31365-3_37","volume-title":"Automated Reasoning","author":"S Schulz","year":"2012","unstructured":"Schulz, S.: Fingerprint indexing for paramodulation and rewriting. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 477\u2013483. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-31365-3_37"},{"key":"31_CR14","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 1.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"},{"key":"31_CR15","unstructured":"Sternagel, T.: Reliable confluence analysis of conditional term rewrite systems. Ph.D. thesis. University of Innsbruck (2017)"},{"key":"31_CR16","doi-asserted-by":"publisher","unstructured":"Sternagel, T., Winkler, S., Zankl, H.: Recording completion for certificates in equational reasoning. In: Proceedings of CPP 2015, pp. 41\u201347 (2015). \nhttps:\/\/doi.org\/10.1145\/2676724.2693171","DOI":"10.1145\/2676724.2693171"},{"issue":"4","key":"31_CR17","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. JAR 43(4), 337\u2013362 (2009). \nhttps:\/\/doi.org\/10.1007\/s10817-009-9143-8","journal-title":"JAR"},{"key":"31_CR18","unstructured":"Winkler, S.: A ground joinability criterion for ordered completion. In: Proceedings of 6th IWC, pp. 45\u201349 (2017)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T12:44:09Z","timestamp":1530276249000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}