{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:45:50Z","timestamp":1743029150205,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031635007"},{"type":"electronic","value":"9783031635014"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T00:00:00Z","timestamp":1719878400000},"content-version":"vor","delay-in-days":183,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Unification has been introduced in Description Logic (DL) as a means to detect redundancies in ontologies. In particular, it was shown that testing unifiability in the DL <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal{E}\\mathcal{L}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                    <mml:mrow>\n                      <mml:mi>E<\/mml:mi>\n                      <mml:mi>L<\/mml:mi>\n                    <\/mml:mrow>\n                  <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is an NP-complete problem, and this result has been extended in several directions. Surprisingly, it turned out that the complexity increases to PSpace if one disallows the use of the top concept in concept descriptions. Motivated by features of the medical ontology SNOMED\u00a0CT, we extend this result to a setting where the top concept is disallowed, but there is a background ontology consisting of restricted forms of concept and role inclusion axioms. We are able to show that the presence of such axioms does not increase the complexity of unification without top, i.e., testing for unifiability remains a PSpace-complete problem.<\/jats:p>","DOI":"10.1007\/978-3-031-63501-4_15","type":"book-chapter","created":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:02:00Z","timestamp":1719824520000},"page":"279-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Unification in\u00a0the\u00a0Description Logic $$\\mathcal {ELH}_{\\mathcal {R}^+}$$ Without the\u00a0Top Concept Modulo Cycle-Restricted Ontologies"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4049-221X","authenticated-orcid":false,"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9458-1701","authenticated-orcid":false,"given":"Oliver","family":"Fern\u00e1ndez Gil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Baader, F., Binh, N.T., Borgwardt, S., Morawska, B.: Unification in the description logic $$\\cal{EL}$$ without the top concept. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 70\u201384. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_8","key":"15_CR1","DOI":"10.1007\/978-3-642-22438-6_8"},{"unstructured":"Baader, F., Borgwardt, S., Morawska, B.: Extending unification in $$\\cal{EL}$$ towards general tboxes. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference (KR 2012), Rome, 10\u201314 June 2012. AAAI Press (2012)","key":"15_CR2"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in $$\\cal{ELH}_{R+}$$ w.r.t. cycle-restricted ontologies. In: Thielscher, M., Zhang, D. (eds.) AI 2012. LNCS (LNAI), vol. 7691, pp. 493\u2013504. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35101-3_42","key":"15_CR3","DOI":"10.1007\/978-3-642-35101-3_42"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification in $$\\cal{ELH}_{R^+}$$ w.r.t. cycle-restricted ontologies. LTCS-Report 12-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit\u00e4t Dresden, Dresden (2012). https:\/\/doi.org\/10.25368\/2022.189","key":"15_CR4","DOI":"10.25368\/2022.189"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: SAT encoding of unification in $$\\cal{ELH}_{{R}^+}$$ w.r.t. cycle-restricted ontologies. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 30\u201344. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_5","key":"15_CR5","DOI":"10.1007\/978-3-642-31365-3_5"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: SAT encoding of unification in $$\\cal{ELH}_{R^+}$$ w.r.t. cycle-restricted ontologies. LTCS-Report 12-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit\u00e4t Dresden, Dresden (2012). https:\/\/doi.org\/10.25368\/2022.186","key":"15_CR6","DOI":"10.25368\/2022.186"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Borgwardt, S., Morawska, B.: Constructing SNOMED CT concepts via disunification. LTCS-Report 17-07, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit\u00e4t Dresden, Dresden (2017). https:\/\/doi.org\/10.25368\/2022.237","key":"15_CR7","DOI":"10.25368\/2022.237"},{"unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $$\\cal{EL}$$ envelope. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI 2005), Edinburgh, 30 July\u20135 August 2005, pp. 364\u2013369. Professional Book Center (2005)","key":"15_CR8"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Fern\u00e1ndez Gil, O.: Unification in the description logic $$\\cal{ELH}_{\\cal{R}^{+}}$$ without the top concept modulo cycle-restricted ontologies (extended version). In: LTCS-Report 24-01, Chair for Automata Theory, Institute of Theoretical Computer Science, Technische Universit\u00e4t Dresden, Dresden (2024). https:\/\/doi.org\/10.25368\/2024.34","key":"15_CR9","DOI":"10.25368\/2024.34"},{"doi-asserted-by":"crossref","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017)","key":"15_CR10","DOI":"10.1017\/9781139025355"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Kapur, D.: Deciding the word problem for ground identities with commutative and extensional symbols. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 163\u2013180. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_10","key":"15_CR11","DOI":"10.1007\/978-3-030-51074-9_10"},{"issue":"6","key":"15_CR12","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1017\/S0960129519000185","volume":"30","author":"F Baader","year":"2020","unstructured":"Baader, F., Marantidis, P., Mottet, A., Okhotin, A.: Extensions of unification modulo ACUI. Math. Struct. Comput. Sci. 30(6), 597\u2013626 (2020). https:\/\/doi.org\/10.1017\/S0960129519000185","journal-title":"Math. Struct. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Mendez, J., Morawska, B.: UEL: unification solver for the description logic $$\\cal{EL}$$\u2014system description. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 45\u201351. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_6","key":"15_CR13","DOI":"10.1007\/978-3-642-31365-3_6"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Morawska, B.: Unification in the description logic $$\\cal{EL}$$. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 350\u2013364. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_25","key":"15_CR14","DOI":"10.1007\/978-3-642-02348-4_25"},{"doi-asserted-by":"publisher","unstructured":"Baader, F., Morawska, B.: SAT encoding of unification in $$\\cal{EL}$$. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 97\u2013111. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_8","key":"15_CR15","DOI":"10.1007\/978-3-642-16242-8_8"},{"doi-asserted-by":"crossref","unstructured":"Baader, F., Morawska, B.: Unification in the description logic $$\\cal EL\\it $$. Log. Methods Comput. Sci. 6(3) (2010)","key":"15_CR16","DOI":"10.2168\/LMCS-6(3:17)2010"},{"issue":"3","key":"15_CR17","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1006\/jsco.2000.0426","volume":"31","author":"F Baader","year":"2001","unstructured":"Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31(3), 277\u2013305 (2001)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"15_CR18","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1215\/00294527-3555507","volume":"57","author":"F Baader","year":"2016","unstructured":"Baader, F., Nguyen, T.B., Borgwardt, S., Morawska, B.: Deciding unifiability and computing local unifiers in the description logic $$\\cal{EL} $$ without top constructor. Notre Dame J. Formal Log. 57(4), 443\u2013476 (2016)","journal-title":"Notre Dame J. Formal Log."},{"doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 445\u2013532. Elsevier and MIT Press (2001)","key":"15_CR19","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ramakrishnan, I.V., Tiwari, A., Vigneron, L.: Congruence closure modulo associativity and commutativity. In: Kirchner, H., Ringeissen, C. (eds.) FroCoS 2000. LNCS (LNAI), vol. 1794, pp. 245\u2013259. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10720084_16","key":"15_CR20","DOI":"10.1007\/10720084_16"},{"doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201017","key":"15_CR21","DOI":"10.3233\/FAIA201017"},{"unstructured":"Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and - what else? In: Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004), Including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, 22\u201327 August 2004, pp. 298\u2013302. IOS Press (2004)","key":"15_CR22"},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0020-0190(05)80006-7","volume":"40","author":"T Jiang","year":"1991","unstructured":"Jiang, T., Ravikumar, B.: A note on the space complexity of some decision problems for finite automata. Inf. Process. Lett. 40(1), 25\u201331 (1991)","journal-title":"Inf. Process. Lett."},{"doi-asserted-by":"crossref","unstructured":"Kapur, D.: Modularity and combination of associative commutative congruence closure algorithms enriched with semantic properties. Log. Methods Comput. Sci. 19(1) (2023)","key":"15_CR24","DOI":"10.46298\/lmcs-19(1:19)2023"},{"issue":"1","key":"15_CR25","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/BF00247671","volume":"17","author":"P Narendran","year":"1996","unstructured":"Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. J. Autom. Reason. 17(1), 131\u2013143 (1996)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"15_CR26","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"WJ Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177\u2013192 (1970). https:\/\/doi.org\/10.1016\/S0022-0000(70)80006-X","journal-title":"J. Comput. Syst. Sci."},{"unstructured":"Schulz, S., Romacker, M., Hahn, U.: Part-whole reasoning in medical ontologies revisited\u2014introducing SEP triplets into classification-based description logics. In: AMIA 1998, American Medical Informatics Association Annual Symposium. AMIA (1998)","key":"15_CR27"},{"unstructured":"Sofronie-Stokkermans, V.: Locality and subsumption testing in $$\\cal{EL}$$ and some of its extensions. In: Advances in Modal Logic 7, papers from the Seventh Conference on Advances in Modal Logic, pp. 315\u2013339. College Publications (2008)","key":"15_CR28"},{"doi-asserted-by":"publisher","unstructured":"Suntisrivaraporn, B., Baader, F., Schulz, S., Spackman, K.: Replacing SEP-triplets in SNOMED CT using tractable description logic operators. In: Bellazzi, R., Abu-Hanna, A., Hunter, J. (eds.) AIME 2007. LNCS (LNAI), vol. 4594, pp. 287\u2013291. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73599-1_38","key":"15_CR29","DOI":"10.1007\/978-3-540-73599-1_38"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63501-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T09:04:20Z","timestamp":1719824660000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63501-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031635007","9783031635014"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63501-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"2 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}