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 | {N^I}, 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
Individuals
individual name	a	a^I
Roles
atomic role	R	R^I
inverse role	R⁻	{⟨x, y⟩ \| ⟨y, x⟩ ∈ R^I}
universal role	U	∆^I × ∆^I
Concepts atomic concept	A	A^I
intersection	C ⊓ D	C^I ∩ D^I
union	C ⊔ D	C^I ∪ D^I
complement	¬C	∆^I \ C^I
top concept	⊤	∆^I
bottom concept	⊥	∅
existential restriction	∃R.C	{x \| some R^I-successor of x is in C^I}
universal restriction	∀R.C	{x \| all R^I-successors of x are in C^I}
at-least restriction	⩾n R.C	{x \| at least n R^I-successors of x are in C^I}
at-most restriction	⩽n R.C	{x \| at most n R^I-successors of x are in C^I}
local reflexivity	∃R.Self	{x \| ⟨x, x⟩ ∈ R^I}
nominal	{a}	{a^I}

where a, b ∈ N^I are individual names, A ∈ N_C is a concept name, C, D ∈ C are concepts, R ∈ R is a role