{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:55:46Z","timestamp":1743004546553,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>On the one hand, equational reasoning is a fundamental part of automated theorem proving with ordered completion as a key technique. On the other hand, the complexity of corresponding, often highly optimized, automated reasoning tools makes implementations inherently error-prone. As a remedy, we provide a formally verified certifier for ordered completion based techniques. This certifier is code generated from an accompanying Isabelle\/HOL formalization of ordered rewriting and ordered completion incorporating an advanced ground joinability criterion. It allows us to rigorously validate generated proof certificates from several domains: ordered completion, satisfiability in equational logic, and confluence of conditional term rewriting.<\/jats:p>","DOI":"10.1007\/978-3-030-29436-6_30","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"508-525","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Certified Equational Reasoning via Ordered Completion"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9864-1014","authenticated-orcid":false,"given":"Christian","family":"Sternagel","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8114-3107","authenticated-orcid":false,"given":"Sarah","family":"Winkler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"issue":"1\u20132","key":"30_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. J. Symb. Comput. 36(1\u20132), 217\u2013233 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00024-5","journal-title":"J. Symb. Comput."},{"key":"30_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","journal-title":"Cambridge University Press"},{"key":"30_CR3","doi-asserted-by":"publisher","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, vol. 2, pp. 1\u201330. Academic Press (1989). https:\/\/doi.org\/10.1016\/B978-0-12-046371-8.50007-9","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-319-63046-5_27","volume-title":"Automated Deduction \u2013 CADE 26","author":"H Becker","year":"2017","unstructured":"Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: A transfinite Knuth\u2013Bendix order for lambda-free higher-order terms. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 432\u2013453. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_27"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"key":"30_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). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.19","DOI":"10.4230\/LIPIcs.FSCD.2017.19"},{"issue":"1","key":"30_CR7","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/0890-5401(90)90023-B","volume":"86","author":"D Kapur","year":"1990","unstructured":"Kapur, D., Narendran, P., Otto, F.: On ground-confluence of term rewriting systems. Inform. Comput. 86(1), 14\u201331 (1990). https:\/\/doi.org\/10.1016\/0890-5401(90)90023-B","journal-title":"Inform. Comput."},{"key":"30_CR8","doi-asserted-by":"publisher","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 (1970). https:\/\/doi.org\/10.1016\/B978-0-08-012975-4","DOI":"10.1016\/B978-0-08-012975-4"},{"key":"30_CR9","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). https:\/\/doi.org\/10.1007\/3-540-52885-7_100"},{"issue":"3","key":"30_CR10","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. Reasoning 19(3), 263\u2013276 (1997). https:\/\/doi.org\/10.1023\/A:1005843212881","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"30_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1020542009983","volume":"29","author":"W McCune","year":"2002","unstructured":"McCune, W., Veroff, R., Fitelson, B., Harris, K., Feist, A., Wos, L.: Short single axioms for Boolean algebra. J. Autom. Reasoning 29(1), 1\u201316 (2002). https:\/\/doi.org\/10.1023\/A:1020542009983","journal-title":"J. Autom. Reasoning"},{"key":"30_CR12","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-21401-6_10","volume-title":"Automated Deduction - 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 (LNAI), vol. 9195, pp. 152\u2013162. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_10"},{"issue":"e24","key":"30_CR14","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. J. Funct. Program. 27(e24), 51 (2017). https:\/\/doi.org\/10.1017\/S0956796817000168","journal-title":"J. Funct. Program."},{"key":"30_CR15","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Sternagel, T.: Certifying confluence of almost orthogonal CTRSs via exact tree automata completion. In: Proceedings of the 1st FSCD. LIPIcs, vol. 52, pp. 29:1\u201329:16. Schloss Dagstuhl (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.29","DOI":"10.4230\/LIPIcs.FSCD.2016.29"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-642-15205-4_39","volume-title":"Computer Science Logic","author":"C Sternagel","year":"2010","unstructured":"Sternagel, C., Thiemann, R.: Signature extensions preserve termination. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 514\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_39"},{"key":"30_CR17","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: Proceedings of the 24th RTA. LIPIcs, vol. 21, pp. 287\u2013302. Schloss Dagstuhl (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.287","DOI":"10.4230\/LIPIcs.RTA.2013.287"},{"key":"30_CR18","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Proceedings of the 11th UITP. EPTCS, vol. 167, pp. 61\u201372 (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"30_CR19","unstructured":"Sternagel, C., Winkler, S.: Certified ordered completion. In: Proceedings of the 7th IWC (2018), arXiv:1805.10090"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-319-08918-8_31","volume-title":"Rewriting and Typed Lambda Calculi","author":"T Sternagel","year":"2014","unstructured":"Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 456\u2013465. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_31"},{"key":"30_CR21","doi-asserted-by":"publisher","unstructured":"Sternagel, T., Winkler, S., Zankl, H.: Recording completion for certificates in equational reasoning. In: Proceedings of the 4th CPP, pp. 41\u201347 (2015). https:\/\/doi.org\/10.1145\/2676724.2693171","DOI":"10.1145\/2676724.2693171"},{"issue":"4","key":"30_CR22","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. J. Autom. Reasoning 43(4), 337\u2013362 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9143-8","journal-title":"J. Autom. Reasoning"},{"key":"30_CR23","unstructured":"Winkler, S.: A ground joinability criterion for ordered completion. In: Proceedings of the 6th IWC, pp. 45\u201349 (2017)"},{"key":"30_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-319-94205-6_31","volume-title":"Automated Reasoning","author":"S Winkler","year":"2018","unstructured":"Winkler, S., Moser, G.: M\u00e6dMax: a maximal ordered completion tool. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 472\u2013480. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_31"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:56:49Z","timestamp":1657576609000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}