Description Logic SROIQ

Origin. Horrocks, Kutz, Sattler (2006). Foundation for OWL 2 DL. Extends ALC with: role hierarchies, transitivity, nominals, inverse, qualified cardinality. Most expressive decidable DL in wide use.

Models. Full OWL 2 expressiveness. Complex role inclusions. Self-restrictions. N2EXPTIME but practical reasoners exist.

Formalism.

S: ALC + transitivity: Trans(R): role R is transitive.

R: role hierarchies: R ⊑ S: role inclusion R ∘ S ⊑ T: role chain (with restrictions) R⁻: inverse role

O: nominals: {a}: singleton concept (nominal) Allows ABox reasoning in TBox.

I: inverse roles: R⁻: inverse of R (R⁻)ᴵ = {(y,x) | (x,y) ∈ Rᴵ}

Q: qualified cardinality: ≥n R.C: at least n R-successors in C ≤n R.C: at most n R-successors in C =n R.C: exactly n R-successors in C

Additional features: Self: ∃R.Self (reflexive R to self) Disjoint roles: Disj(R, S) Reflexive, irreflexive, symmetric, asymmetric roles.

Regular role inclusions: R₁ ∘ ... ∘ Rₙ ⊑ R Must satisfy regularity condition (acyclicity).

Example — complex role inclusion: hasParent ∘ hasBrother ⊑ hasUncle "A brother of one's parent is one's uncle." This is the canonical SROIQ example and shows precisely what R adds: the left-hand chain is inexpressible in SHOIQ. Regularity is met, since hasUncle does not itself occur on the left.

Example — concept definition: Uncle ≡ Male ⊓ ∃hasSibling.∃hasChild.⊤ "A male who has a sibling who has a child." Note ∃hasChild.⊤, not ∃hasChild.Self. Self is only ever written ∃R.Self and asserts an R-loop at the individual itself, so ∃hasChild.Self would say the individual is its own child; it is not a filler and cannot stand where a concept is expected.

Symbols.

Metatheory. SROIQ is sound and complete for the standard description-logic semantics restricted to interpretations satisfying the RBox conditions. Horrocks, Kutz and Sattler (2006) gave a terminating tableau decision procedure, and Kazakov (2008) settled the complexity: knowledge base satisfiability is N2ExpTime-complete, one exponential above SHOIQ, which is NExpTime-complete. Decidability rests on two syntactic side conditions rather than on the semantics. Complex role inclusions must form a regular set — acyclic under a strict order on role names — because unrestricted role chains make satisfiability undecidable; and number restrictions, role disjointness, irreflexivity and Self may mention only simple roles, those not implied by any composition, because counting over transitive roles is likewise undecidable. Nominals destroy the tree model property, so the decision procedure works over forest-shaped models with a bounded nominal core. SROIQ lacks the finite model property: inverse roles with functionality force infinite chains, so a satisfiable knowledge base can have no finite model.

Applies to. OWL 2 ontologies. Biomedical ontologies. Enterprise knowledge. Semantic web. Data integration.

Limitations. The decidability of SROIQ rests entirely on syntactic restrictions that also cut expressiveness: role chains that are not regular, and counting or Self or disjointness applied to a non-simple role, must be rejected rather than merely reasoned about slowly, since either yields an undecidable logic. Failure of the finite model property means a knowledge base can be satisfiable while having no finite model, so SROIQ entailment does not coincide with entailment over finite domains and cannot be read as constraining a database. Roles are binary, so genuinely n-ary relations must be reified. The semantics remains open-world and monotone, with no unique name assumption, no closed-world negation and no defaults; adding unrestricted rules over variables, as in unrestricted SWRL, is undecidable, and only the DL-safe fragment is admissible. OWL 2 Full, which drops the separation of classes, properties and individuals, is undecidable.

© 2026 Lingenic LLC