{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:48:51Z","timestamp":1743140931157,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We revisit AC completion for left-linear term rewrite systems where AC unification is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. Finally, we present experimental results for our implementation of left-linear AC completion in the tool .<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_23","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"401-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Left-Linear Completion with\u00a0AC Axioms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8662-6834","authenticated-orcid":false,"given":"Johannes","family":"Niederhauser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8499-0501","authenticated-orcid":false,"given":"Nao","family":"Hirokawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7366-8464","authenticated-orcid":false,"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-79351-6","volume-title":"Reduktionssysteme","author":"J Avenhaus","year":"1995","unstructured":"Avenhaus, J.: Reduktionssysteme. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/978-3-642-79351-6. (in German)"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","key":"23_CR2","DOI":"10.1017\/CBO9781139172752"},{"doi-asserted-by":"publisher","unstructured":"Bachmair, L.: Canonical Equational Proofs. Progress in Theoretical Computer Science. Birkh\u00e4user, Boston (1991). https:\/\/doi.org\/10.1007\/978-1-4684-7118-2","key":"23_CR3","DOI":"10.1007\/978-1-4684-7118-2"},{"doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A., Sternagel, C., Winkler, S.: Abstract completion, formalized. Logical Methods Comput. Sci. 15(3), 19:1\u201319:42 (2019). https:\/\/doi.org\/10.23638\/LMCS-15(3:19)2019","key":"23_CR4","DOI":"10.23638\/LMCS-15(3:19)2019"},{"issue":"4","key":"23_CR5","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980). https:\/\/doi.org\/10.1145\/322217.322230","journal-title":"J. ACM"},{"issue":"4","key":"23_CR6","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"JP Jouannaud","year":"1986","unstructured":"Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155\u20131194 (1986). https:\/\/doi.org\/10.1137\/0215084","journal-title":"SIAM J. Comput."},{"doi-asserted-by":"publisher","unstructured":"Kapur, D.: A modular associative commutative (AC) congruence closure algorithm. In: Kobayashi, N. (ed.) Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 195, pp. 15:1\u201315:21 (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.15","key":"23_CR7","DOI":"10.4230\/LIPIcs.FSCD.2021.15"},{"issue":"1","key":"23_CR8","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"6","author":"D Kapur","year":"1988","unstructured":"Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered in the Knuth-Bendix completion procedure. J. Symb. Comput. 6(1), 19\u201336 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80019-1","journal-title":"J. Symb. Comput."},{"doi-asserted-by":"publisher","unstructured":"Klein, D., Hirokawa, N.: Maximal completion. In: Schmidt-Schau\u00df, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 10, pp. 71\u201380 (2011). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.71","key":"23_CR9","DOI":"10.4230\/LIPIcs.RTA.2011.71"},{"doi-asserted-by":"publisher","unstructured":"Knuth, D.E., Bendix, P.B.: 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.50028-X","key":"23_CR10","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-02348-4_21","volume-title":"Rewriting Techniques and Applications","author":"M Korp","year":"2009","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295\u2013304. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21"},{"issue":"3","key":"23_CR12","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1006\/jsco.1996.0011","volume":"21","author":"C March\u00e9","year":"1996","unstructured":"March\u00e9, C.: Normalized rewriting: an alternative to rewriting modulo a set of equations. J. Symb. Comput. 21(3), 253\u2013288 (1996). https:\/\/doi.org\/10.1006\/jsco.1996.0011","journal-title":"J. Symb. Comput."},{"doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In: Raamsdonk, F. (ed.) Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 21, pp. 286\u2013301 (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.287","key":"23_CR13","DOI":"10.4230\/LIPIcs.RTA.2013.287"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-642-31365-3_41","volume-title":"Automated Reasoning","author":"T Sternagel","year":"2012","unstructured":"Sternagel, T., Zankl, H.: KBCV \u2013 Knuth-Bendix completion visualizer. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 530\u2013536. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_41"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11805618_22","volume-title":"Term Rewriting and Applications","author":"I Wehrman","year":"2006","unstructured":"Wehrman, I., Stump, A., Westbrook, E.: Slothrop: Knuth-Bendix completion with a modern termination checker. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 287\u2013296. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_22"},{"unstructured":"Winkler, S.: Termination tools in automated reasoning. Ph.D. thesis, University of Innsbruck (2013)","key":"23_CR16"},{"doi-asserted-by":"publisher","unstructured":"Winkler, S.: Extending maximal completion. In: Geuvers, H. (ed.) Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics, vol. 131, pp. 3:1\u20133:15 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.3","key":"23_CR17","DOI":"10.4230\/LIPIcs.FSCD.2019.3"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-22438-6_37","volume-title":"Automated Deduction \u2013 CADE-23","author":"S Winkler","year":"2011","unstructured":"Winkler, S., Middeldorp, A.: AC completion with termination tools. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 492\u2013498. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_37"},{"doi-asserted-by":"publisher","unstructured":"Winkler, S., Middeldorp, A.: Normalized completion revisited. In: Raamsdonk, F. (ed.) Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics, vol. 21, pp. 318\u2013333 (2013). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.319","key":"23_CR19","DOI":"10.4230\/LIPIcs.RTA.2013.319"},{"issue":"3","key":"23_CR20","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10817-012-9249-2","volume":"50","author":"S Winkler","year":"2013","unstructured":"Winkler, S., Sato, H., Middeldorp, A., Kurihara, M.: Multi-completion with termination tools. J. Autom. Reason. 50(3), 317\u2013354 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9249-2","journal-title":"J. Autom. Reason."},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-319-08918-8_32","volume-title":"Rewriting and Typed Lambda Calculi","author":"A Yamada","year":"2014","unstructured":"Yamada, A., Kusakari, K., Sakabe, T.: Nagoya Termination Tool. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 466\u2013475. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_32"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:05:19Z","timestamp":1693609519000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","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":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}