We are pursuing our work on Standpoint logics (SL) in relation and independently from knowledge evolution.
In prior work we had shown that it is possible to add standpoints to numerous decidable fragments of first-order logics – including very expressive DLs up to $\mathcal{SROIQB}_s$ – while preserving their reasoning complexity, so long as standpoint modalities are limited to the axiom level. A more expressive tighter modal integration, where standpoint modalities are also allowed to occur in concept expressions, had so far only been investigated for the much less expressive $\mathcal{EL}+$ logic.
We pushed this line of research further, showing that the $\mathcal{SHIQ}$ logic allows for a tight modal integration with standpoints without compromising its ExpTime reasoning complexity [Gómez Álvarez 2024a]. The core insight toward this result is that any satisfiable knowledge base admits a model with only polynomially many worlds. This allowed us to establish a polynomial equisatisfiable translation into plain $\mathcal{SHIQ}$ which, beyond showing the theoretical result, enables us to use highly optimised OWL reasoners to provide practical reasoning support for ontology languages extended by standpoint modelling.
Standpoint extensions of knowledge representation 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 have considered the extension of $\mathcal{C}^2$ – the counting two-variable fragment of first-order logic – by monodic standpoints [Gómez Álvarez 2025a]. At the core of this work was a polytime translation of formulae in standpoint logic into standpoint-free $\mathcal{C}^2$, which required elaborate model-theoretic arguments. By virtue of this translation, the NEXPTIME-complete complexity of checking satisfiability in $\mathcal{C}^2$ carried over to our formalism. As this work subsumed monodic S5 over $\mathcal{C}^2$, the results also significantly advanced the state of the art in research on first-order modal logics. As a practical consequence, the very expressive description logics $\mathcal{SHOIQB}_s$ and $\mathcal{SROIQB}_s$, which subsume the popular W3C-standardized OWL 1 and OWL 2 ontology languages, were shown to allow for monodic standpoint extensions without any increase of standard reasoning complexity. We proved that NEXPTIME-hardness already occurred in much less expressive description logics as long as they featured both nominals and monodic standpoints. We also showed that, with inverses, functionality, and nominals present, minimally lifting the monodicity restriction led to undecidability.
Many complex scenarios require the coordination of agents possessing different points of view, and thus may involve reasoning across both conflicting perspectives and temporal dynamics. To address this need, standpoint linear temporal logic (SLTL) provides a framework combining standpoint logic with linear temporal logic (LTL), a well-established formalism for specifying temporal properties of systems and processes.
In this work, we took a significant step beyond the previous theoretical work on SLTL and provided automated reasoning support for the logic. We did this by introducing a SAT-based approach for checking the satisfiability of SLTL formulae. This consisted of producing a SAT encoding that emulates the behaviour of a tableau algorithm for SLTL up to a depth $k$ in an incremental fashion, in what is known as bounded satisfiability checking. Our algorithm was implemented as an extension of the BLACK satisfiability checker, a state-of-the-art SAT-based LTL solver. In order to evaluate the feasibility of the approach, we introduced the first benchmark set for SLTL, which included a diverse and scalable collection of formulae designed to evaluate solver performance and scalability.
We have started adapting belief revision to standpoint logics. We introduce four dynamic operators inspired from the equivalent operators of dynamic epistemic logic: Public announcements for standpoint logic, private announcements for standpoint logic, simple radical update for standpoint logic, and memoryless radical update for standpoint logic. These new operators are compatible with the semantic structures of Standpoint Logic. We showed that extending standpoint logics with public and private announcements preserves the NP-completeness of its satisfiability problem.
| Publications on standpoint logic |