Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A New Tractable Description Logic under Categorical Semantics

Chan Le Duc, Ludovic Brieulle

TL;DR

This work introduces a category-theoretic foundation for Description Logics to represent negative knowledge without sacrificing tractability. By identifying and dropping independent semantic properties responsible for intractability, the authors derive $\mathcal{EL}^{\rightarrow}$, a tractable extension of $\mathcal{EL}$ that exceeds $\mathcal{EL}_{\bot}^{\circ}$ in expressiveness. The core contribution is a categorical semantics that separates the meaning of constructors (via products, coproducts, adjoints, and arrows) from standard set membership, enabling a deterministic, polynomial-time reasoning approach. This approach promises practical applicability to biomedical ontologies and suggests avenues for implementing specialized reasoners (e.g., Arrow) and extending the framework to richer DL constructs and query answering.

Abstract

Biomedical ontologies contain numerous concept or role names involving negative knowledge such as lacks_part, absence_of. Such a representation with labels rather than logical constructors would not allow a reasoner to interpret lacks_part as a kind of negation of has_part. It is known that adding negation to the tractable Description Logic (DL) EL allowing for conjunction, existential restriction and concept inclusion makes it intractable since the obtained logic includes implicitly disjunction and universal restriction which interact with other constructors. In this paper, we propose a new extension of EL with a weakened negation allowing to represent negative knowledge while retaining tractability. To this end, we introduce categorical semantics of all logical constructors of the DL SH including EL with disjunction, negation, universal restriction, role inclusion and transitive roles. The categorical semantics of a logical constructor is usually described as a set of categorical properties referring to several objects without using set membership. To restore tractability, we have to weaken semantics of disjunction and universal restriction by identifying \emph{independent} categorical properties that are responsible for intractability, and dropping them from the set of categorical properties. We show that the logic resulting from weakening semantics is more expressive than EL with the bottom concept, transitive roles and role inclusion.

A New Tractable Description Logic under Categorical Semantics

TL;DR

This work introduces a category-theoretic foundation for Description Logics to represent negative knowledge without sacrificing tractability. By identifying and dropping independent semantic properties responsible for intractability, the authors derive , a tractable extension of that exceeds in expressiveness. The core contribution is a categorical semantics that separates the meaning of constructors (via products, coproducts, adjoints, and arrows) from standard set membership, enabling a deterministic, polynomial-time reasoning approach. This approach promises practical applicability to biomedical ontologies and suggests avenues for implementing specialized reasoners (e.g., Arrow) and extending the framework to richer DL constructs and query answering.

Abstract

Biomedical ontologies contain numerous concept or role names involving negative knowledge such as lacks_part, absence_of. Such a representation with labels rather than logical constructors would not allow a reasoner to interpret lacks_part as a kind of negation of has_part. It is known that adding negation to the tractable Description Logic (DL) EL allowing for conjunction, existential restriction and concept inclusion makes it intractable since the obtained logic includes implicitly disjunction and universal restriction which interact with other constructors. In this paper, we propose a new extension of EL with a weakened negation allowing to represent negative knowledge while retaining tractability. To this end, we introduce categorical semantics of all logical constructors of the DL SH including EL with disjunction, negation, universal restriction, role inclusion and transitive roles. The categorical semantics of a logical constructor is usually described as a set of categorical properties referring to several objects without using set membership. To restore tractability, we have to weaken semantics of disjunction and universal restriction by identifying \emph{independent} categorical properties that are responsible for intractability, and dropping them from the set of categorical properties. We show that the logic resulting from weakening semantics is more expressive than EL with the bottom concept, transitive roles and role inclusion.
Paper Structure (7 sections, 24 theorems, 15 equations, 3 figures)

This paper contains 7 sections, 24 theorems, 15 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Set-theoretical Semantics of DLs
  3. Categorical semantics
  4. Categorical Consistency
  5. A new tractable extension $\mathcal{EL}^{\rightarrow}$ of $\mathcal{EL}$
  6. Related Work
  7. Conclusion and Future Work

Key Result

Lemma 1

$S'\subseteq (S\circ S)^\mathcal{I}$ if for all $S"\subseteq S'$ there are $S_1,S_2\subseteq S^\mathcal{I}$ such that $\Pi_\ell(S")=\Pi_\ell(S_1)$, $\Pi_r(S")=\Pi_r(S_2)$ and $\Pi_r(S_1)=\Pi_\ell(S_2)$.

Figures (3)

  • Figure 1: A portion of $\mathbf{T}$
  • Figure 2: A portion of $\mathbf{T}$
  • Figure 3: When a branch node $x_{W\cdot 0}$ is generated, the part of $T_{W\cdot 0}$ from level 0 to level $(k-1)$ is no longer changed. Furthermore, tableau rules applied to $T_{W\cdot 0}$ can change only the subtree of $T_{W\cdot 0}$ rooted at $x_{W\cdot 0}$ until a next application of $\sqcup$-rule to some node $x'_{W\cdot 0}$ located at a level higher than $(k-1)$.

Theorems & Definitions (60)

  • Example 1
  • Definition 1: syntax categories
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • proof
  • Example 2
  • Lemma 4
  • ...and 50 more