This paper is an extended abstract of our recent work on proposing a stable model semantics for Description Logic terminologies. Our semantics is based on Quantified Equilibrium Logic and overcomes some limitations of previous approaches. We prove that standard reasoning problems w.r.t. terminologies in ℒℐ under the stable model semantics are decidable in deterministic single exponential time. In contrast, we show that concept satisfiability w.r.t. general KBs in ℒℐ under the stable model semantics is undecidable.
(ii) PrivilegedUser(), PrivilegedUser()
While the extension (i) is natural and expected, the extension (ii) is questionable: the membership of
and in PrivilegedUser is not well-founded (there is only a self-supported justification). Baader [
QEL is based on Here-and-There Logic (HT) with an additional minimality requirement. In contrast to the classical case, an interpretation in the logic HT consists of a pair of structures (ℐ, ) sharing the same domain and interpreting individuals in the same way. The interpretation ℐ is the ‘here’ world while is the ‘there’ world. We call assumed everything that is true ‘there’, and founded everything that is true ‘here’. The two ‘worlds’ are related by the inclusion relation, i.e. ℐ ⊆ : ‘here’ is included in ‘there’, i.e. ℐ ⊆ , for all predicates . Fixed predicates can be easily expressed by requiring that ℐ and agree on a set of predicates. In this case, we write ℐ ⊆ .
Definition 1. A Here-and-There (HT) interpretation is a pair (ℐ, ) of interpretations with ℐ ⊆ . We define an interpretation function · (ℐ, ) using the equations in Figure 1.
In the HT logic, the implication is intuitionistic: in jargon it needs to be ‘founded’, meaning that the HT interpretation must model it, and ‘assumed’, meaning that the ‘there’ world must model it. In DLs, the universally quantified concept of the form ∀. can be translated in FOL as ∀(((, ) → ()). Thus the interpretation must align with the interpretation of implication in quantified HT. As a matter of fact, concept inclusions are also afected by this double nature of implication, as they are ‘explicit’ implications in DLs.
Definition 2.
Assume a KB = ( , ) and an HT interpretation (ℐ, ). We write: (ℐ, ) = ℐ (ℐ, ) = ℐ
(ℐ, ) = ℐ (− )(ℐ, ) = {(, ′) | (′, ) ∈ ℐ } (1 ⊓ 2)(ℐ, ) = 1(ℐ, ) ∩ 2(ℐ, ) ⊤(ℐ, ) = Δℐ (¬)(ℐ, ) = Δℐ ∖
⊥(ℐ, ) = ∅ (1 ⊔ 2)(ℐ, ) = 1(ℐ, ) ∪ 2(ℐ, ) (∃.)(ℐ, ) = { ∈ Δℐ | ∃′ : (, ′) ∈ (ℐ, ) ∧ ′ ∈ (ℐ, )} (∀.)(ℐ, ) = {︁ ∈ Δℐ | ∀′ : ((,, ′′)) ∈∈ (ℐ,im)pilmiepslie′s∈′∈(ℐ, ) and }︁ - (ℐ, ) |= ⊑ , if (ℐ, ) ⊆ (ℐ, ) and ⊆ ; - (ℐ, ) |= , if ℐ |= and (ℐ, ) |= ⊑ , for all ⊑ ∈ .
Definition 3 (Stable model). Given ⊆ ∪ , an interpretation is a stable model of a KB under fixed predicates , if (i) the HT interpretation ( , ) is a model of , and (ii) there is no ℐ s.t. (ℐ, ) is a model of and ℐ ⊂ .
Intuitively, a model is stable if it cannot be further improved in a better ‘here’ world. In the semantics introduced above, the negation ¬ behaves as negation as failure or default negation in logic programs. Given an HT model, the ‘there’ is a classical model and a concept true at some domain element in the ‘there’ can be thought of as ‘to be justified’. An HT model is not stable if the truth of an atom in the ‘there’ cannot be proved. Intuitively, the truth of ¬ at a domain element in a stable model amounts to ‘we cannot justify at ’.
The standard reasoning tasks of satisfiability , concept satisfiability , subsumption and instance checking
are adapted to stable models in the obvious way [
Theorem 1. Concept satisfiability in ℒℐ under the stable model semantics is undecidable.
The result above is based on a reduction from the domino problem. The constructed TBox is
negationfree, thus the undecidability result applies to circumscribed ℒℐ with all predicates minimized,
extending the results of [
Terminologies. A key feature of terminologies is the separation of the predicates in a terminology into two sets: def( ) are the intensional predicates that are defined using concept definitions based on the extensional predicates in base( ). In the context of the stable model semantics, it is thus natural to not require minimization of the predicates in base( ), i.e. the extensions of these predicates should remain fixed during the minimization process. Based on this observation, a stable model semantics for terminologies can be immediately obtained by instantiating Definition 3, which covers general KBs: (a) view every concept definition := ∈ as an inclusion ⊑ , and (b) use = base( ) as the set of fixed predicates.
In [
Theorem 2. If a terminology has a stable model, then it has a tree-shaped stable model.
Given a terminology , we can construct a 2ATA A (with Büchi acceptance condition) whose number of states is polynomial in the size of and such that has a tree-shaped stable model if A is not empty, i.e. A accepts a tree. The automaton A is the intersection of two automata on labeled trees. The first automaton A checks that the input tree is a classical model of the terminology, it can be constructed in the usual way [12]. The second automaton A checks the well-foundedness of defined concepts and can be constructed in a similar way of [13].
Theorem 3. For ℒℐ terminologies under the stable model semantics, the problems of satisfiability, concept subsumption, and concept satisfiability are ExpTime-complete.
We expect that our result for terminologies in ℒℐ can be extended to ℒℐ following the techniques of [13]. Finite model reasoning in terminologies under the stable model semantics is also a relevant open problem: it has the potential to provide new insights into, e.g., the complexity of static analysis problems for SHACL. Another natural direction (also relevant for SHACL) is to study terminologies that support regular expressions over roles, which enable recursive navigation of paths in an interpretation.
This work was partially supported by the Austrian Science Fund (FWF) project P30873, and by the Wallenberg AI, Autonomous Systems, and Software Program (WASP), funded by the Knut and Alice Wallenberg Foundation. [11] M. Andresel, J. Corman, M. Ortiz, J. L. Reutter, O. Savkovic, M. Šimkus, Stable model semantics for recursive SHACL, in: Proc. of WWW 2020, ACM / IW3C2, 2020, pp. 1570–1580. [12] D. Calvanese, T. Eiter, M. Ortiz, Answering regular path queries in expressive description logics:
An automata-theoretic approach, in: Proc. of AAAI 2007, AAAI Press, 2007, pp. 391–396. [13] U. Sattler, M. Y. Vardi, The hybrid -calculus, in: Proc. of IJCAR 2001, volume 2083 of Lecture Notes in Computer Science, Springer, 2001, pp. 76–91. URL: https://doi.org/10.1007/3-540-45744-5_7. doi:10.1007/3-540-45744-5\_7.