=Paper= {{Paper |id=Vol-3739/abstract-25 |storemode=property |title=Stable Model Semantics for Description Logic Terminologies (Extended Abstract) |pdfUrl=https://ceur-ws.org/Vol-3739/abstract-25.pdf |volume=Vol-3739 |authors=Federica Di Stefano,Mantas Ε imkus |dblpUrl=https://dblp.org/rec/conf/dlog/0001S24a }} ==Stable Model Semantics for Description Logic Terminologies (Extended Abstract)== https://ceur-ws.org/Vol-3739/abstract-25.pdf 
                         Stable Model Semantics for Description Logic
                         Terminologies (Extended Abstract)
                         Federica Di Stefano1 , Mantas Ε imkus1,2
                         1
                             Institute of Logic and Computation, Vienna University of Technology, Austria
                         2
                             Department of Computing Science, UmeΓ₯ University, Sweden


                                        Abstract
                                        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.

                                        Keywords
                                        Stable Models, Quantified Equilibrium Logic, Terminologies, Computational Complexity




                         1. Introduction and Motivation
                         Description Logics are often seen as fragments of the classical first-order logic, equipped with a syntax
                         that is more convenient for knowledge representation [1]. In particular, this means that most DLs
                         nowadays make the open-world assumption (OWA), in which, intuitively, everything that is not forbidden
                         is considered possible. However, it is acknowledged that supporting the closed-world assumption (CWA)
                         is also important in order to enable commonsense reasoning in DLs, e.g., by means of default negation
                         (see, e.g., the overview and the references in [2]). In [3], we consider Description Logics under the
                         stable model semantics of Quantified Equilibrium Logic (QEL) [4] which provides an elegant logical
                         formalization of the stable model semantics of logic programs with default negation [5]. The stable model
                         semantics of QEL turns out to be an appropriate semantics for terminologies in π’œβ„’π’žβ„. A terminology 𝒯
                         consists of statements of the form 𝐴 := 𝐢, where a concept name 𝐴 is defined using a complex concept
                         expression 𝐢. A terminology may contain terminological cycles, where a definition of some concept
                         name may be recursive, as in the following terminology:

                                                                     BasicUser := User βŠ“ Β¬PrivilegedUser
                                                             PrivilegedUser := Admin βŠ” βˆƒpromotedBy.PrivilegedUser

                         Here BasicUser and PrivilegedUser are (intensional or defined) concept names defined using (exten-
                         sional) base predicates User , Admin, and promotedBy. A concrete semantics for terminologies tells us
                         how to interpret the defined concept names given an extension for the base predicates. Suppose the
                         base predicates correspond to the following facts:

                                                             User (π‘Ž) User (𝑏) promotedBy(π‘Ž, 𝑏) promotedBy(𝑏, π‘Ž)

                         In the last three decades, essentially three semantics have been proposed to deal with terminologies:
                         the least fixpoint semantics, the greatest fixpoint semantics, and the descriptive semantics. The descriptive
                         semantics [6] is nowadays the classical semantics for DLs, deemed as the most natural semantics and it
                         sees β€œ:=” as a logical equivalence; in our example, it produces two possible extensions for the defined
                         concept names:
                                (i) BasicUser(π‘Ž), BasicUser(𝑏)
                            DL 2024: 37th International Workshop on Description Logics, June 18–21, 2024, Bergen, Norway
                          $ federica.stefano@tuwien.ac.at (F. Di Stefano); simkus@dbai.tuwien.ac.at (M. Ε imkus)
                                        Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
 (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 [7]
advocates fixpoint semantics to overcome some weaknesses of the descriptive semantics. However, the
semantics of Baader is too strong in this example: it rejects both (i) and (ii). The stable model semantics
based on QEL proposed in [3] is stronger than the classical semantics, in the sense that some classical
models of a KB or terminology will be rejected as implausible (like (ii) in our example above), and
accepts (i). Enabling default negation, the stable model semantics of QEL allows to combine the OWA
and the CWA in a natural way. The reconciliation of OWA and CWA specifically in DL terminologies is
a problem whose relevance is boosted by the new W3C SHACL standard for expressing constraints
over RDF graphs [8]. SHACL is syntactically very close to DL terminologies, but its semantics has not
been fully established yet (but it clearly leans towards CWA). The main contributions of [3] can be
summarized as follows:

    β€’ We define a semantics for general DL knowledge bases using Quantified Equilibrium Logic
      (QEL) [4]. The use of QEL in defining the semantics allows us to elegantly support fixed predicates,
      which are needed for modeling (extensional) base predicates in terminologies.
    β€’ We provide a strong undecidability results for reasoning in π’œβ„’π’žβ„π’ͺ and π’œβ„’π’žβ„ in the presence of
      role minimization. In particular, for π’œβ„’π’žβ„π’ͺ the proof is given for KBs without negation, which
      means that it carries over and applies to circumscribed π’œβ„’π’žβ„π’ͺ KBs where all predicates are set
      to be minimized. This complements the negative results in [9], which rely on the use of varying
      predicates.
    β€’ We define a stable model semantics for DL terminologies. To achieve this, we instantiate our
      stable model semantics for general KBs. Intuitively, for a given terminology 𝒯 , we require all
      base concept and role names of 𝒯 to be interpreted as fixed predicates, i.e. they are not subject to
      minimization. In addition, we provide two alternative definitions of stable models, based on level
      mappings and fixpoint computation. We prove that the semantics are equivalent.
    β€’ We study the case of π’œβ„’π’žβ„ terminologies and prove ExpTime-completeness for the standard rea-
      soning tasks. This is achieved by proving a tree-model property and employing 2-way alternating
      tree automata [10].


2. Stable Model Semantics and Contributions
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 affected 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
                  (βˆƒπ‘….𝐢)(ℐ,π’₯ ) = {𝑒 ∈ Δℐ | βˆƒπ‘’β€² : (𝑒, 𝑒′ ) ∈ 𝑅(ℐ,π’₯ ) ∧ 𝑒′ ∈ 𝐢 (ℐ,π’₯ ) }
                                                   (𝑒, 𝑒′ ) ∈ 𝑅(ℐ,π’₯ ) implies 𝑒′ ∈ 𝐢 (ℐ,π’₯ ) and
                                 {︁                                                             }︁
                  (βˆ€π‘….𝐢)(ℐ,π’₯ ) = 𝑒 ∈ Δℐ | βˆ€π‘’β€² :
                                                   (𝑒, 𝑒′ ) ∈ 𝑅π’₯ implies 𝑒′ ∈ 𝐢 π’₯

        Figure 1: HT semantics for DLs.


- (ℐ, π’₯ ) |= 𝐢 βŠ‘ 𝐷, 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 [3]. Identifying a stable model of a KB requires checking
minimality (see (ii) in Definition 3), which is computationally difficult.

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 negation-
free, thus the undecidability result applies to circumscribed π’œβ„’π’žβ„π’ͺ with all predicates minimized,
extending the results of [9] relying on the use of varying predicates. We prove that under the stable
model semantics reasoning w.r.t. KBs in π’œβ„’π’žβ„π’ͺ can be reduced to reasoning w.r.t. KBs in π’œβ„’π’žβ„.
Thus standard reasoning problems in π’œβ„’π’žβ„ are undecidable.

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 [3], we define an equivalent stable model semantics for terminologies based on level mappings,
similarly to [11]. Level mappings allow tracking the justifications of defined predicates. Roughly
speaking, a model of a terminology is stable if all occurrences of defined concepts are well-founded,
meaning that they are supported by a finite justification. We use level mapping to guide the unraveling
of stable models, preserving the well-foundedness.
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 iff 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.


3. Conclusions
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.


Acknowledgments
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.


References
 [1] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
     University Press, 2017. doi:10.1017/9781139025355.
 [2] T. Schneider, M. Ε imkus,         Ontologies and data management: A brief survey,              KΓΌn-
     stliche Intell. 34 (2020) 329–353. URL: https://doi.org/10.1007/s13218-020-00686-3. doi:10.1007/
     S13218-020-00686-3.
 [3] F. Di Stefano, M. Ε imkus, Stable model semantics for description logic terminologies, in: AAAI,
     AAAI Press, 2024, pp. 10484–10492.
 [4] D. Pearce, A. Valverde, Quantified equilibrium logic and foundations for answer set programs, in:
     Proc. of ICLP 2008, volume 5366 of Lecture Notes in Computer Science, Springer, 2008, pp. 546–560.
 [5] D. Pearce, Equilibrium logic, Ann. Math. Artif. Intell. 47 (2006) 3–41.
 [6] B. Nebel, Terminological cycles: Semantics and computational properties, in: J. F. Sowa (Ed.),
     Principles of Semantic Networks - Explorations in the Representation of Knowledge, The Morgan
     Kaufmann Series in representation and reasoning, Morgan Kaufmann, 1991, pp. 331–361. URL: https:
     //doi.org/10.1016/B978-1-4832-0771-1.50018-7. doi:10.1016/B978-1-4832-0771-1.50018-7.
 [7] F. Baader, Terminological cycles in KL-ONE-based knowledge representation languages, in:
     Proc. of AAAI 1990, AAAI Press / The MIT Press, 1990, pp. 621–626.
 [8] H. Knublauch, D. Kontokostas, Shapes constraint language (W3C SHACL), https://www.w3.org/
     TR/shacl/, 2017. Accessed: 2024-01-24.
 [9] P. A. Bonatti, C. Lutz, F. Wolter, The complexity of circumscription in description logic, J. Artif.
     Intell. Res. 35 (2009) 717–773.
[10] M. Y. Vardi, Reasoning about the past with two-way automata, in: Proc. of ICALP 1998, volume
     1443 of Lecture Notes in Computer Science, Springer, 1998, pp. 628–641.
[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.