%0 Conference Paper %1 baader2024unification %A Baader, Franz %A Fernández Gil, Oliver %B Automated Reasoning %C Cham %D 2024 %E Benzmüller, Christoph %E Heule, Marijn J.H. %E Schmidt, Renate A. %I Springer Nature Switzerland %K imported xack %P 279--297 %T Unification in the Description Logic \$\$\backslashmathcal \ELH\\_\\backslashmathcal \R\^+\\$\$Without the Top Concept Modulo Cycle-Restricted Ontologies %X 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 \$\$\backslashmathcal\E\\backslashmathcalŁ\\$\$ELis 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 CT, 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. %@ 978-3-031-63501-4

@inproceedings{baader2024unification, abstract = {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 {\$}{\$}{\backslash}mathcal{\{}E{\}}{\backslash}mathcal{\{}L{\}}{\$}{\$}ELis 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 CT, 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.}, added-at = {2024-12-16T11:07:33.000+0100}, address = {Cham}, author = {Baader, Franz and Fern{\'a}ndez Gil, Oliver}, biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/264669512557fb84a94c9b32c661d04c5/scadsfct}, booktitle = {Automated Reasoning}, editor = {Benzm{\"u}ller, Christoph and Heule, Marijn J.H. and Schmidt, Renate A.}, interhash = {1b7cf3069e0f66b3cb132088e92d3c57}, intrahash = {64669512557fb84a94c9b32c661d04c5}, isbn = {978-3-031-63501-4}, keywords = {imported xack}, pages = {279--297}, publisher = {Springer Nature Switzerland}, timestamp = {2025-02-13T15:02:25.000+0100}, title = {Unification in the Description Logic {\$}{\$}{\backslash}mathcal {\{}ELH{\}}{\_}{\{}{\backslash}mathcal {\{}R{\}}^+{\}}{\$}{\$}Without the Top Concept Modulo Cycle-Restricted Ontologies}, year = 2024 }