The SROIQ(D) Description Logic

The SROIQ(D) description logic roughly corresponds to the set of constructors available in OWL 2. It is one of the most expressive decidable description logics to date, supporting atomic negation, concept intersection, universal restrictions, limited existential quantification, complex class expressions by combining mathematical operators such as subclass relationships, equivalence, conjunction, disjunction, negation, property restrictions, tautology, and contradiction, transitive roles, full existential quantification, functional properties (a special case of uniqueness quantification), concept union, role hierarchy (subproperties), complex role inclusion, reflexivity and irreflexivity, role disjointness, enumerated classes of object value restrictions (nominals), inverse properties, unqualified cardinality restrictions, qualified cardinality restrictions, data type properties, data values, and data types. The price of this high expressivity is the N2EXPTIME worst-case combined complexity.

Definition (SROIQ ontology). A SROIQ ontology is a set O of axioms including ϱ ⊑ R complex role inclusions, Disj(S1, S2) disjoint roles, C ⊑ D concept inclusions, C(a) concept assertions, and R(a,b) role assertions, wherein ϱ is a role chain, R(i) and S(i) are roles, C and D are concepts, and a, b individuals, such that the set of all RIAs in O is ≺-regular for some regular order ≺ on roles.

Definition (SROIQ concept expression). A set of SROIQ concept expressions is defined as C ::= NC | (C⊓C) | (C⊔C) | ¬C | ⊤ | ⊥ | ∃R.C | ∀R.C | ⩾nR.C | ⩽nR.C | ∃R.Self | {NI}, wherein C represents concepts, R is a set of roles, and n is a non-negative integer.

Table 1. Syntax and semantics of SROIQ constructors
Syntax Semantics
individual name a aI
atomic role R RI
inverse role R {⟨x, y⟩ | ⟨y, x⟩ ∈ RI}
universal role U I × ∆I
atomic concept
intersection CD CIDI
union CD CIDI
complement ¬C I \ CI
top concept I
bottom concept
existential restriction R.C {x | some RI-successor of x is in CI}
universal restriction R.C {x | all RI-successors of x are in CI}
at-least restriction ⩾n R.C {x | at least n RI-successors of x are in CI}
at-most restriction ⩽n R.C {x | at most n RI-successors of x are in CI}
local reflexivity R.Self {x | ⟨x, x⟩ ∈ RI}
nominal {a} {aI}

where a, bNI are individual names, A ∈ NC is a concept name, C, DC are concepts, RR is a role