arXiv subjects

Barbara Morawska

Publications and source records attributed to Barbara Morawska.

5 recordsLinked to original sources

arXiv2026

Subsumption in $\mathcal{FL}_{\bot \mathit{reg}}$ with TBoxes Is in ExpTime

Description Logics (DLs) are a family of formal languages used for representing and reasoning about structured knowledge in terms of concepts and their relationships. The expressive power of a DL depends on the constructors available for building complex concepts. In this work, we investigate subsumption in the restricted description logic $\mathcal{FL}_{\bot\mathit{reg}}$ and the related fragments $\mathcal{FL}_{\mathit{reg}}$, $\mathcal{FL}_\bot$, and $\mathcal{FL}_0$. These formalisms support value restrictions over role names, where the subscript $\mathit{reg}$ indicates the use of regular expressions over roles. Subsumption between two concept descriptions in $\mathcal{FL}_{\bot\mathit{reg}}$ and $\mathcal{FL}_{\mathit{reg}}$ is PSpace-complete. When subsumption is considered with respect to a TBox (i.e., a set of axioms), the complexity increases to ExpTime-complete. These results can be derived either from complexity bounds established for more expressive logics or from algorithms designed for harder reasoning problems. We reprove the PSpace-completeness result and provide a new proof of ExpTime-completeness for $\mathcal{FL}_{\mathit{reg}}$ and $\mathcal{FL}_{\bot\mathit{reg}}$ with TBoxes via a novel reduction to parity pushdown games. Our algorithm relies only on the constructs available in these logics and may therefore be implemented more easily.

cs.LO↗

arXiv2025

FILO -- automated unification in $\mathcal{FL}_0$

FILO is a java application that decides unifiability for a unification problem formulated in the description logic $\mathcal{FL}_0$. If the problem is unifiable, it presents a user with an example of a solution. FILO joins a family of similar applications like UEL solving unification problems in the description logic $\mathcal{EL}$, $\mathcal{FL}_0$wer a subsumption decider for $\mathcal{FL}_0$ with TBox, CEL and JCEL subsumption deciders for $\mathcal{EL}$ with TBox, and others. These systems play an important role in various knowledge representation reasoning problems.

cs.LO↗

arXiv2024

Solving unification in the description logic $\mathcal{FL}_\bot$

We present an algorithm for solving the unification problem in the description logic $\mathcal{FL}_\bot$. This logic extends $\mathcal{FL}_0$ with the bottom constructor, and thus supports conjunction, value restrictions, top and bottom constructors. Unification of concepts can be a useful tool for ontology maintenance; however, little is known about unification even in small, restricted description logics. The unification problem has been solved only for $\mathcal{FL}_0$ and $\mathcal{EL}$. This paper contributes to the ongoing effort to extend these results to richer logics. Our algorithm runs in exponential time with respect to the size of the problem.

cs.SC↗

arXiv2016

Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification

Unification in Description Logics has been introduced as a means to detect redundancies in ontologies. We try to extend the known decidability results for unification in the Description Logic $\mathcal{EL}$ to disunification since negative constraints can be used to avoid unwanted unifiers. While decidability of the solvability of general $\mathcal{EL}$-disunification problems remains an open problem, we obtain NP-completeness results for two interesting special cases: dismatching problems, where one side of each negative constraint must be ground, and local solvability of disunification problems, where we consider only solutions that are constructed from terms occurring in the input problem. More precisely, we first show that dismatching can be reduced to local disunification, and then provide two complementary NP-algorithms for finding local solutions of disunification problems.

cs.LO↗

arXiv2010

Unification in the Description Logic EL

The Description Logic EL has recently drawn considerable attention since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. The main result of this paper is that unification in EL is decidable. More precisely, EL-unification is NP-complete, and thus has the same complexity as EL-matching. We also show that, w.r.t. the unification type, EL is less well-behaved: it is of type zero, which in particular implies that there are unification problems that have no finite complete set of unifiers.

cs.AI↗