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: Uncle ≡ ∃hasParent⁻.(Male ⊓ ∃hasSibling.∃hasChild.Self) (Simplified uncle definition)

Symbols.

Symbol	Unicode	Name	Meaning
⁻	—	Inverse	Role inverse
{ }	—	Nominal	Individual as concept
≥n R.C	—	Min cardinality	At least n
≤n R.C	—	Max cardinality	At most n
∘	U+2218	Composition	Role chain
Self	—	Self	Reflexive loop

Metatheory. N2EXPTIME-complete. Decidable via tableau. OWL 2 DL based on SROIQ. Practical reasoners: HermiT, Pellet, FaCT++.

Applies to. OWL 2 ontologies. Biomedical ontologies (SNOMED CT). Enterprise knowledge. Semantic web. Data integration.

Limitations. High worst-case complexity. Role regularity constraints. Some combinations undecidable. Large ontologies challenging.