Putting Perspective into OWL [Sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic

Standpoint extensions of KR formalisms have been recently

introduced to incorporate multi-perspective modelling and

reasoning capabilities. In such modal extensions, the integration of conceptual modelling and perspective annotations

can be more or less tight, with monodic standpoint extensions

striking a good balance as they enable advanced modelling

while preserving good reasoning complexities.

We consider the extension of C² – the counting two-variable

fragment of first-order logic – by monodic standpoints. At

the core of our treatise is a polytime translation of formulae

in said formalism into standpoint-free C², requiring elaborate

model-theoretic arguments. By virtue of this translation, the

NEXPTIME-complete complexity of checking satisfiability in

C² carries over to our formalism. As our formalism subsumes

monodic S5 over C², our result also significantly advances the

state of the art in research on first-order modal logics.

As a practical consequence, the very expressive description

logics ?ℋ?ℐ?ℬs and ?ℛ?ℐ?ℬs which subsume the popular W3C-standardized OWL 1 and OWL 2 ontology languages,

are shown to allow for monodic standpoint extensions without

any increase of standard reasoning complexity.

We prove that NEXPTIME-hardness already occurs in much

less expressive DLs as long as they feature both nominals

and monodic standpoints. We also show that, with inverses,

functionality, and nominals present, minimally lifting the monodicity restriction leads to undecidability.