Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix)

Fuente: arXiv
Gespeichert in:
Bibliographische Detailangaben
Hauptverfasser: Álvarez, Lucía Gómez, Rudolph, Sebastian
Format: Preprint
Veröffentlicht: 2025
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1866918110174380032
author Álvarez, Lucía Gómez
Rudolph, Sebastian
author_facet Álvarez, Lucía Gómez
Rudolph, Sebastian
contents Standpoint extensions of knowledge representation formalisms have been recently introduced as a means to incorporate multi-perspective modelling and reasoning through modal operators that attribute pieces of knowledge to specific entities or agents. In these extensions, the integration between conceptual modelling and perspective annotations can vary in strength, with monodic standpoint extensions offering a well-balanced approach. They allow for advanced modelling features, such as the expression of rigid concepts, while maintaining desirable reasoning complexity. We consider the extension of C2--the counting two-variable fragment of first-order logic--by monodic standpoints. At the heart of our work is a polynomial-time translation of formulas in this extended formalism into standard, standpoint-free C2, a result that relies on intricate model-theoretic arguments. Thanks to this translation, the satisfiability problem remains at the same complexity level: NExpTime-complete, as in plain C2. Since our formalism subsumes monodic S5 over C2, this result also marks a substantial advancement in the study of first-order modal logics. From a practical standpoint, this means that highly expressive description logics such as SHOIQBs and SROIQBs--which underpin the widely adopted OWL 1 and OWL 2 ontology languages standardised by the W3C--can be extended with monodic standpoints without increasing the standard reasoning complexity. We further prove that NExpTime-hardness arises even in significantly less expressive description logics, as long as they include both nominals and monodic standpoints. Moreover, we show that if the monodicity restriction is relaxed even slightly in the presence of inverse roles, functionality, and nominals, the satisfiability problem becomes undecidable.
format Preprint
id arxiv_https___arxiv_org_abs_2508_00653
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix)
Álvarez, Lucía Gómez
Rudolph, Sebastian
Logic in Computer Science
Standpoint extensions of knowledge representation formalisms have been recently introduced as a means to incorporate multi-perspective modelling and reasoning through modal operators that attribute pieces of knowledge to specific entities or agents. In these extensions, the integration between conceptual modelling and perspective annotations can vary in strength, with monodic standpoint extensions offering a well-balanced approach. They allow for advanced modelling features, such as the expression of rigid concepts, while maintaining desirable reasoning complexity. We consider the extension of C2--the counting two-variable fragment of first-order logic--by monodic standpoints. At the heart of our work is a polynomial-time translation of formulas in this extended formalism into standard, standpoint-free C2, a result that relies on intricate model-theoretic arguments. Thanks to this translation, the satisfiability problem remains at the same complexity level: NExpTime-complete, as in plain C2. Since our formalism subsumes monodic S5 over C2, this result also marks a substantial advancement in the study of first-order modal logics. From a practical standpoint, this means that highly expressive description logics such as SHOIQBs and SROIQBs--which underpin the widely adopted OWL 1 and OWL 2 ontology languages standardised by the W3C--can be extended with monodic standpoints without increasing the standard reasoning complexity. We further prove that NExpTime-hardness arises even in significantly less expressive description logics, as long as they include both nominals and monodic standpoints. Moreover, we show that if the monodicity restriction is relaxed even slightly in the presence of inverse roles, functionality, and nominals, the satisfiability problem becomes undecidable.
title Putting Perspective into OWL [sic]: Complexity-Neutral Standpoint Reasoning for Ontology Languages via Monodic S5 over Counting Two-Variable First-Order Logic (Extended Version with Appendix)
topic Logic in Computer Science
url https://arxiv.org/abs/2508.00653