SROIQ

Overview

\mathcal{SROIQ} is a highly expressive description logic developed by Horrocks, Kutz and Sattler. It extends expressive DLs with nominals, inverse roles, qualified number restrictions, and regular complex role inclusions. It forms the logical foundation of OWL 2 DL (subject to OWL's precise syntactic and datatype restrictions). Its expressiveness comes with demanding reasoning complexity.

Concept Language

A representative grammar is

\begin{aligned} C ::={}&\top\mid\bot\mid A\mid\neg C\mid(C\sqcap C)\mid(C\sqcup C)\\ &\mid\exists R.C\mid\forall R.C\mid\{a\}\\ &\mid\geq n\,S.C\mid\leq n\,S.C\mid\exists S.\mathsf{Self}. \end{aligned}

Here A is a concept name, R is a permitted (possibly inverse) role, \{a\} is a singleton nominal, and S must be a simple role for number restrictions and self restrictions. Role names, inverses and role axioms are constrained by well-formedness restrictions.

Role Hierarchies and Global Restrictions

SROIQ supports complex role inclusions, for example

\mathit{hasParent}\circ\mathit{hasBrother} \sqsubseteq\mathit{hasUncle}.

The meaning is that a parent followed by a brother determines an uncle relation. To preserve decidability, the role hierarchy must satisfy a regularity condition, and constructs such as qualified number restrictions, local reflexivity and certain role characteristics are restricted to simple roles. These conditions are essential, not mere implementation advice.

Semantics

An interpretation I=(\Delta^I,\cdot^I) maps concept names to subsets of the domain, role names to binary relations, and individuals to domain elements. Nominals denote singletons \{a^I\}. For counting,

(\geq n\,S.C)^I =\{x\in\Delta^I:|\{y:(x,y)\in S^I\land y\in C^I\}|\geq n\}.

A role-chain inclusion R_1\circ R_2\sqsubseteq R means R_1^I\circ R_2^I\subseteq R^I. Knowledge bases contain a TBox of general concept inclusions, an RBox of role axioms, and an ABox of assertions. Standard OWL-style DL semantics is open-world, and different individual names do not by themselves imply distinct individuals.

Example

The axioms \mathit{Doctor}\sqsubseteq\mathit{Person} and \mathit{Doctor}\sqsubseteq\geq1\,\mathit{worksAt}.\mathit{Hospital} express that every doctor is a person and works at at least one hospital. The second axiom creates an existential commitment in models, not necessarily a named database fact.

Decidability and Complexity

Under the standard SROIQ global syntactic restrictions, classical knowledge-base reasoning (including consistency and concept satisfiability in the usual setting) is N2EXPTIME-complete (nondeterministic double exponential time). This is not the EXPTIME bound of ALC. Subfragments may be substantially cheaper; for example, certain Horn-SROIQ query-answering problems have polynomial data complexity under explicitly stated assumptions.

Relationships

ALC is a fundamental less expressive DL. DLP isolates a rule-friendly Horn overlap rather than the entirety of SROIQ; Horn-SROIQ and OWL 2 RL impose additional syntactic restrictions. 3DL is based on defeasible ALC, and its EXPTIME minimal-entailment result must not be assumed for a hypothetical defeasible-SROIQ combination.

References

1. Ian Horrocks, Oliver Kutz, and Ulrike Sattler (2006). The Even More Irresistible SROIQ. KR 2006. PDF.
2. Yevgeny Kazakov (2008). RIQ and SROIQ Are Harder than SHOIQ. KR 2008. PDF.
3. W3C (2012). OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax (Second Edition). Recommendation.
4. Magdalena Ortiz, Sebastian Rudolph, and Mantas Šimkus (2011). Query Answering in the Horn Fragments of the Description Logics SHOIQ and SROIQ. IJCAI 2011. DOI.