Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

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 EL 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 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.

Details

Original languageEnglish
Title of host publicationAutomated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 1-6, 2024, Proceedings, Part II
EditorsChristoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
PublisherSpringer
Pages279-297
Number of pages19
Publication statusPublished - 2 Jul 2024
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume14740
ISSN0302-9743

Conference

Title12th International Joint Conference on Automated Reasoning
Abbreviated titleIJCAR 2024
Conference number12
Duration1 - 6 July 2024
Website
Degree of recognitionInternational event
LocationUniversité de Lorraine
CityNancy
CountryFrance

External IDs

ORCID /0000-0002-4049-221X/work/163766175

Keywords

Keywords

  • Complexity, Description Logics, Unification