{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T04:04:33Z","timestamp":1751342673655,"version":"3.40.5"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2019,11,11]],"date-time":"2019-11-11T00:00:00Z","timestamp":1573430400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The theory ACUI of an associative, commutative, and idempotent binary function symbol + with unit<jats:bold>0<\/jats:bold>was one of the first equational theories for which the complexity of testing solvability of unification problems was investigated in detail. In this paper, we investigate two extensions of ACUI. On one hand, we consider approximate ACUI-unification, where we use appropriate measures to express how close a substitution is to being a unifier. On the other hand, we extend ACUI-unification to ACUIG-unification, that is, unification in equational theories that are obtained from ACUI by adding a finite set<jats:italic>G<\/jats:italic>of ground identities. Finally, we combine the two extensions, that is, consider approximate ACUI-unification. For all cases we are able to determine the exact worst-case complexity of the unification problem.<\/jats:p>","DOI":"10.1017\/s0960129519000185","type":"journal-article","created":{"date-parts":[[2019,11,11]],"date-time":"2019-11-11T10:53:50Z","timestamp":1573469630000},"page":"597-626","source":"Crossref","is-referenced-by-count":4,"title":["Extensions of unification modulo ACUI"],"prefix":"10.1017","volume":"30","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1934-5741","authenticated-orcid":false,"given":"Pavlos","family":"Marantidis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antoine","family":"Mottet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Okhotin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2019,11,11]]},"reference":[{"key":"S0960129519000185_ref4","unstructured":"Baader, F. , K\u00fcsters, R. and Molitor, R. (1999). Computing least common subsumers in description logics with existential restrictions. In: Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI 1999), 96\u2013101."},{"key":"S0960129519000185_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2015.10.004"},{"key":"S0960129519000185_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2014.07.006"},{"key":"S0960129519000185_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02127747"},{"key":"S0960129519000185_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129519000185_ref2","unstructured":"Baader, F. , Borgwardt, S. and Morawska, B. (2012). Extending unification in \u2130\u2112 towards general TBoxes. In: Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR 2012), AAAI Press\/The MIT Press, 568\u2013572."},{"key":"S0960129519000185_ref12","first-page":"447","volume-title":"Handbook of Automated Reasoning","author":"Baader","year":"2001"},{"key":"S0960129519000185_ref20","unstructured":"Lehmann, K. and Turhan, A.-Y. (2012). A framework for semantic-based similarity measures for \u2130\u2112\u210b-concepts. In: Proceedings of the 13th European Conference on Logics in Artificial Intelligence (JELIA\u20192012), vol. 7519. Lecture Notes in Computer Science. Springer, 307\u2013319."},{"key":"S0960129519000185_ref13","first-page":"645","article-title":"Set unification","volume":"6","author":"Dovier","year":"2006","journal-title":"TPLP"},{"key":"S0960129519000185_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245463"},{"key":"S0960129519000185_ref5","unstructured":"Baader, F. , Marantidis, P. and Okhotin, A. (2016). Approximate unification in the description logic \u2131\u21120. In: Michael, L. and Kakas, A. C. (eds.) Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA 2016), vol. 10021. Lecture Notes in Artificial Intelligence. Springer, 49\u201363."},{"key":"S0960129519000185_ref10","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0009"},{"key":"S0960129519000185_ref11","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/oso\/9780198537465.003.0002","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"Baader","year":"1994"},{"key":"S0960129519000185_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16780-3_113"},{"key":"S0960129519000185_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90028-7"},{"key":"S0960129519000185_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"S0960129519000185_ref21","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0011"},{"volume-title":"Computers and Intractability; A Guide to the Theory of NP-Completeness","year":"1990","author":"Garey","key":"S0960129519000185_ref15"},{"key":"S0960129519000185_ref3","unstructured":"Baader, F. , Fern\u00e1ndez Gil, O. and Marantidis, P. (2018). Matching in the description logic {\u21950 with respect to general TBoxes. In: Barthe, G. , Sutcliffe, G. and Veanes, M. (eds.) Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2018), vol. 57. EPiC Series in Computing, EasyChair, 76\u201394."},{"key":"S0960129519000185_ref7","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2000.0426"},{"key":"S0960129519000185_ref6","unstructured":"Baader, F. and Morawska, B. (2009). Unification in the description logic \u2130\u2112. In: Treinen, R. (ed.) Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), vol. 5595. Lecture Notes in Computer Science. Springer, 350\u2013364."},{"key":"S0960129519000185_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BF00247671"},{"key":"S0960129519000185_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-65340-2_56"},{"key":"S0960129519000185_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80012-4"},{"key":"S0960129519000185_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56730-5_29"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129519000185","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T18:02:00Z","timestamp":1722016920000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129519000185\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,11]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["S0960129519000185"],"URL":"https:\/\/doi.org\/10.1017\/s0960129519000185","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2019,11,11]]}}}