=Paper=
{{Paper
|id=Vol-3739/paper-10
|storemode=property
|title=Translating Equilibrium Description Logics into Circumscription
|pdfUrl=https://ceur-ws.org/Vol-3739/paper-10.pdf
|volume=Vol-3739
|authors=Federica Di Stefano,Mantas Šimkus
|dblpUrl=https://dblp.org/rec/conf/dlog/0001S24
}}
==Translating Equilibrium Description Logics into Circumscription==
<pdf width="1500px">https://ceur-ws.org/Vol-3739/paper-10.pdf</pdf>
<pre>
                         Translating Equilibrium Description Logics into
                         Circumscription
                         Federica Di Stefano1 , Mantas Šimkus1
                         1
                             Institute of Logic and Computation, TU Wien, Austria


                                        Abstract
                                        Circumscription is a powerful framework for enabling non-monotonic reasoning in Description Logics (DLs) and
                                        other knowledge representation languages based on first-order logic. It is very expressive and rather abstract,
                                        which is why it is often used as a host language for defining other non-monotonic formalisms. An alternative
                                        approach to obtain a non-monotonic version of a given first-order knowledge representation language is the
                                        Equilibrium Logic (EL). For instance, EL allows the generalization of the stable model semantics of logic programs
                                        to arbitrary propositional theories and even to arbitrary first-order theories. Recently, DLs with semantics based
                                        on EL have been proposed in the context of DL terminologies, but a deeper understanding of this formalism is still
                                        missing. The goal of this paper is to clarify the connection been DLs based on EL and DLs based on circumscription,
                                        both under the well-known global circumscription and the recently proposed pointwise circumscription. To this
                                        end, we first introduce a simple yet powerful extension of circumscribed DLs by attaching to a circumscribed KB
                                        an additional set of axioms, which filter out unintended minimal models of the first KB. As we show in this paper,
                                        such constrained circumscription is powerful enough to capture DLs under the EL semantics, with global and
                                        pointwise minimality. We argue that in some important cases, constrained circumscription is computationally
                                        not more expensive than its base variant. Together with the proposed translation, this provides new decidability
                                        and complexity results for DLs based on EL semantics.

                                        Keywords
                                        Minimal Model Reasoning, Circumscription, Pointwise Minimality, Quantified Equilibrium Logic




                         1. Introduction
                         Description Logics (DLs), as fragments of first-order logic, are monotonic. A prominent research line
                         on extending DLs with non-monotonic features is given by circumscribed DLs [1, 2, 3, 4]. At the core of
                         circumscription – whether it is applied to DLs or other languages based on first-order logic – there is
                         predicate minimization: classical models are filtered by circumscription, selecting the so-called minimal
                         models where the extension of some predicates is the minimal possible. To perform such selection, a
                         knowledge base (KB) is equipped with a circumscription pattern which partitions the set of predicates
                         into minimized, varying, and fixed predicates and induces a preference relation among models. The
                         freedom of selecting how to treat predicates, by selecting an appropriate circumscription pattern, makes
                         circumscribed DLs a very expressive formalism. Circumscription is often used as a host language for
                         defining other non-monotonic formalisms, e.g. for defeasible inclusions in DLs [5]. A disadvantage
                         of circumscribed DLs is given by the high computational costs. Remarkably, the arity of minimized
                         predicates and the interaction with varying predicates affects the decidability of basic reasoning tasks:
                         allowing roles to be minimized makes concept satisfiability undecidable already in 𝒜ℒ𝒞 [1]. To reduce
                         the complexity of reasoning, pointwise circumscription has been proposed in [6]. The main difference
                         between circumscription and pointwise circumscription is how predicate minimization is performed. In
                         circumscription, predicates are allowed to be globally minimized across the model. For this reason, we
                         refer to standard circumscription as global circumscription. While, in pointwise circumscription, the
                         global minimization is replaced by local minimizations performed at the single domain elements [6].
                            Along the line of predicate minimization, another prominent approach is given by Equilibrium
                         Description Logics (EDLs) [7] based on Quantified Equilibrium Logic (QEL) [8, 9]. QEL provides logical
                         foundations to the stable model semantics of logic programs, allowing to extend it to arbitrary theories

                            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
in first-order logic. In [7], the stable model semantics based on QEL is used for DL terminologies, i.e.
collections of possibly recursive concept definitions, ultimately showing that for terminologies in 𝒜ℒ𝒞ℐ
the basic reasoning tasks can be performed in deterministic single exponential time. In particular, the
stable model semantics based on QEL overcomes some limitations of previous works [10, 11], where
terminologies are required to be syntactically monotonic. In contrast with the terminologies case,
concept satisfiability w.r.t. general knowledge bases in 𝒜ℒ𝒞ℐ is proved to be undecidable [7]. A key
feature of DL terminologies is the partition of predicates into two sets: intensional predicates, subjected
to minimization, and extensional predicates, that behave classically, meaning that (in the jargon of
circumscription) they are fixed, and always contain the roles occurring in the terminology. Having
classical roles, paired with the observation that terminologies correspond to a syntactic fragment of
general knowledge bases in 𝒜ℒ𝒞ℐ, plays a crucial role when it comes to decidability.
   The main contributions of this work are as follows.
∘ We study the connection between circumscribed DLs and EDLs. Although both are based on predicate
minimization, circumscribed DLs and EDLs are two ‘orthogonal’ formalisms with different features, e.g.
varying predicates of circumscribed DLs vs. default negation of EDLs. We show that an EDL knowledge
base can be transformed into a circumscribed knowledge base such that there is a correspondence
between the stable models of the first and a restricted set of models of the second one. Specifically, this
restricted set of models is obtained by filtering out those models satisfying a further set of inclusions.
∘ To formalize such additional restrictions, we propose a hybrid form of circumscription where a
circumscribed knowledge base is paired with a non-circumscribed one. This second knowledge base
acts as a filter over the set of minimal models, allowing further refinement of the selection process
of minimal models. We call this formalism constrained circumscription, as the non-circumscribed
knowledge base constraints the model selection. A similar idea has been used in [6] where a pointwise
circumscribed knowledge base is equipped with a set of constraints, mimicking concept inclusions,
which are used for the normalization of complex concepts. We show that constrained circumscription
enhances the expressive power of circumscription, in some cases without an additional computational
cost.
∘ We define a pointwise stable model semantics where a pointwise minimization (in the style of pointwise
circumscription) is performed. We extend the translation aforementioned. In particular, we show that a
pointwise EDL KB can be translated into a pointwise circumscribed KB with constraints such that there
is a correspondence between the pointwise minimal models of the second KB and stable models of the
first.
∘ We extend the undecidability results in [7] showing that concept satisfiability w.r.t. EDL KBs in 𝒜ℒ𝒞
and pointwise EDL KBs in 𝒜ℒ𝒞ℐ is undecidable.


2. Preliminaries
We focus on 𝒜ℒ𝒞ℋℐ𝒪 for its expressiveness and recall here the basic notions needed in the following.
We call NC , NR , and NI the mutually disjoint sets of concept names, role names, and individuals. The
expression 𝑟− is the inverse role of a role name 𝑟 ∈ NR . The syntax of complex concepts in 𝒜ℒ𝒞ℋℐ𝒪
is defined by the grammar 𝐶 := ⊤ | ⊥ | 𝐴 | {𝑎} | ¬𝐶 | 𝐶 ⊔ 𝐶 | 𝐶 ⊓ 𝐶 | ∃𝑟.𝐶 | ∀𝑟.𝐶, with 𝐴 ∈ NC ,
𝑟 ∈ NR or 𝑟 = 𝑠− with 𝑠 ∈ NR , and 𝑎 ∈ NI . A TBox 𝒯 is a finite set of concept inclusions and role
inclusions, which are expressions of the form 𝐶 ⊑ 𝐷 and 𝑟 ⊑ 𝑠, respectively, with 𝐶 and 𝐷 concepts,
and 𝑟 and 𝑠 role names or inverse roles. An expression of the form 𝐴(𝑎), where 𝐴 ∈ NC and 𝑎 ∈ NI ,
is a concept assertion, while an expression of the form 𝑟(𝑎, 𝑏) is a role assertion, where 𝑟 ∈ NR . An ABox
𝒜 is a collection of assertions. A knowledge base (KB) is a pair 𝒦 = (𝒜, 𝒯 ), where 𝒜 is an ABox and 𝒯
is a TBox. Given a KB 𝒦, we denote with 𝑠𝑖𝑔(𝒦) the set of concept names, role names, and individual
names occurring in 𝒦. The classical semantics of 𝒜ℒ𝒞ℋℐ𝒪 is defined by means of interpretations
ℐ = (Δℐ , ·ℐ ) where Δℐ is the domain and ·ℐ the interpretation function associating to each 𝑎 ∈ NI a
unique element 𝑎ℐ ∈ Δℐ , to each 𝐴 ∈ NC a set 𝐴ℐ ⊆ Δℐ and to each 𝑟 ∈ NR a set 𝑟ℐ ⊆ Δℐ × Δℐ . The
extension of remaining concept and role expressions in 𝒜ℒ𝒞ℐ𝒪 is defined as usual [12]. In this work,
we adopt the unique name assumption. The notion of a (classical) model of a KB, TBox, or ABox is also
standard (as usual, we use ‘|=’ for this). We refer to [12] for further details and fragments considered in
the following.


3. Global and Pointwise Circumscription
We use [1] and [6] as main references respectively for circumscribed and pointwise circumscribed
DLs. Given a KB, when we apply circumscription, beforehand we declare a circumscription pattern
𝒫 = (𝑀, 𝑉, 𝐹 ) defining which predicates are minimized, varying or fixed. Circumscription then simply
selects the models fulfilling the requirement of the circumscription pattern, i.e. those models where the
extension of the minimized predicates cannot be further reduced without violating some axioms. Thus,
at the core of circumscription, there is the idea of comparing structures and discriminating which one
we have to prefer.

Definition 1. Given a set 𝐹 ⊆ NC ∪ NR and two interpretations ℐ and 𝒥 , we write ℐ ∼𝐹 𝒥 if

 (i) Δℐ = Δ𝒥 ,

 (ii) 𝑎ℐ = 𝑎𝒥 , for all individuals 𝑎 ∈ 𝑁𝐼 ,

(iii) 𝑞 ℐ = 𝑞 𝒥 , for all 𝑞 ∈ 𝐹 .

   The above definition simply groups interpretations sharing the same domain, interpreting individuals
in the same way, and agreeing on the set of predicates in 𝐹 . Note that 𝐹 can be empty. In this case, we
simply write ℐ ∼ 𝒥 .
   We now formalize the preference relation naturally induced by circumscription patterns. Formally,
a circumscription pattern is a triple 𝒫 = (𝑀, 𝑉, 𝐹 ) where 𝑀, 𝑉 and 𝐹 are mutually disjoint sets of
minimized, varying and fixed predicates.

Definition 2 (Preference relation). Given a circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ) and two interpreta-
tions ℐ, 𝒥 such that ℐ ∼𝐹 𝒥 , we write:

    • ℐ ⪯𝒫 𝒥 if 𝑝ℐ ⊆ 𝑝𝒥 , for all 𝑝 ∈ 𝑀 ;

    • ℐ ≺𝒫 𝒥 , if ℐ ⪯𝒫 𝒥 and 𝑝ℐ ⊂ 𝑝𝒥 for some 𝑝 ∈ 𝑀 .

If the circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ) is such that 𝑉 = ∅, we denote the relations ⪯𝒫 and ≺𝒫
with the symbols ⊆𝐹 and ⊂𝐹 , respectively.

   Given a KB 𝒦, a circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ) for 𝒦 is a partition of the predicates
occurring in 𝒦. A KB 𝒦 equipped with a circumscription pattern 𝒫 is called circumscribed and we
denote it with Circ𝒫 (𝒦). Given a circumscribed KB, we aim to filter the set of all possible models
selecting those where the extension of minimized predicates is the smallest possible.

Definition 3. (Minimal model) An interpretation ℐ is a minimal model of Circ𝒫 (𝒦), in symbols ℐ |=
Circ𝒫 (𝒦), if ℐ |= 𝒦 and there is no interpretation 𝒥 s.t. 𝒥 |= 𝒦 and 𝒥 ≺𝒫 ℐ. We use MM (𝒦, 𝒫) to
denote the set of minimal models of Circ𝒫 (𝒦).

   Observe that Definition 2 does not restrict how the extension of 𝑝 may differ in ℐ and 𝒥 and
varying predicates do not occur in any of the conditions. Thus, when searching for minimal models,
circumscription allows for the reconfiguration of the predicates across the entire model.
   In [6] an approximation of circumscription based on pointwise circumscription [13] has been introduced.
Differently from (global) circumscription, in pointwise circumscription [13] predicates can be minimized
only locally at a given tuple of domain elements. In [6] the minimization can only affect a domain
element and the roles it participates in, leaving the rest of the structure unmodified. By repeatedly
applying such local minimizations, we can often replicate the minimization across the entire model of
       𝑎(ℐ,𝒥 ) = 𝑎ℐ         𝐴(ℐ,𝒥 ) = 𝐴ℐ               𝑟(ℐ,𝒥 ) = 𝑟ℐ   ⊤(ℐ,𝒥 ) = Δℐ            ⊥(ℐ,𝒥 ) = ∅
                      (𝑟− )(ℐ,𝒥 ) = {(𝑒, 𝑒′ ) | (𝑒′ , 𝑒) ∈ 𝑟ℐ }        (¬𝐶)(ℐ,𝒥 ) = Δℐ ∖ 𝐶 𝒥
                                       (ℐ,𝒥 )      (ℐ,𝒥 )                                 (ℐ,𝒥 )      (ℐ,𝒥 )
               (𝐶1 ⊓ 𝐶2 )(ℐ,𝒥 ) = 𝐶1            ∩ 𝐶2                  (𝐶1 ⊔ 𝐶2 )(ℐ,𝒥 ) = 𝐶1        ∪ 𝐶2
                  (∃𝑅.𝐶)(ℐ,𝒥 ) = {𝑒 ∈ Δℐ | ∃𝑒′ : (𝑒, 𝑒′ ) ∈ 𝑅(ℐ,𝒥 ) ∧ 𝑒′ ∈ 𝐶 (ℐ,𝒥 ) }
                                                   (𝑒, 𝑒′ ) ∈ 𝑅(ℐ,𝒥 ) implies 𝑒′ ∈ 𝐶 (ℐ,𝒥 ) and
                                 {︁                                                             }︁
                  (∀𝑅.𝐶)(ℐ,𝒥 ) = 𝑒 ∈ Δℐ | ∀𝑒′ :
                                                   (𝑒, 𝑒′ ) ∈ 𝑅𝒥 implies 𝑒′ ∈ 𝐶 𝒥

        Figure 1: HT semantics for DLs, with 𝑎 ∈ NI , 𝐴 ∈ NC and 𝑟 ∈ NR .


classical circumscription, but not always: pointwise circumscription is not able to minimize predicate
participating in a cycle and treats varying predicates differently. See [6, 3] for detailed comments on
the differences between the two formalisms for DLs.

Definition 4. Given two interpretations ℐ and 𝒥 we write ℐ ∼∙ 𝒥 if there exists 𝑒 ∈ Δℐ s.t.:

    • for all 𝐴 ∈ NC , 𝐴ℐ ∖ {𝑒} = 𝐴𝒥 ∖ {𝑒}, and

    • for all 𝑟 ∈ NR , 𝑟ℐ ∩ (Δ × Δ) = 𝑟𝒥 ∩ (Δ × Δ), with Δ = Δℐ ∖ {𝑒}.

   Thus, two interpretations in the relation ∼∙ may differ in terms of concept and role names involving
one domain element. We now use the relation in Definition 4 to give a pointwise flavor to the preference
relation between interpretations of Definition 2.

Definition 5. Assume a circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ) and two interpretations ℐ, 𝒥 such that
ℐ ∼𝐹 𝒥 . We write

    • ℐ ⪯∙𝒫 𝒥 , if ℐ ∼∙ 𝒥 and ℐ ⪯𝒫 𝒥 ;

    • ℐ ≺∙𝒫 𝒥 , if ℐ ⪯∙𝒫 𝒥 and 𝑝ℐ ⊂ 𝑝𝒥 for some 𝑝 ∈ 𝑀 .

Given a circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ) such that 𝑉 = ∅, we denote ⪯∙𝒫 and ≺∙𝒫 with ⊆∙𝐹 and
⊂∙𝐹 , respectively.

Definition 6. An interpretation ℐ is a pointwise minimal model of Circ𝒫 (𝒦), in symbols ℐ |=∙ Circ𝒫 (𝒦),
if ℐ |= 𝒦 and there is no interpretation 𝒥 s.t. 𝒥 |= 𝒦 and 𝒥 ≺∙𝒫 ℐ. We use PMM (𝒦, 𝒫) to denote the
set of pointwise minimal models of Circ𝒫 (𝒦).

  The standard definitions of concept satisfiability, concept subsumption, and concept instances are
adapted to (resp. pointwise) minimal models in the obvious way and can be reduced polynomial one into
the other [1, 6]. In this work, we focus on concept satisfiability w.r.t. (resp. pointwise) circumscribed
KBs: given a concept 𝐶 and a circumscribed KB Circ𝒫 (𝒦), we write Circ𝒫 (𝒦) |=(∙) 𝐶, if 𝐶 ℐ ̸= ∅
holds for some ℐ ∈ MM (𝒦, 𝒫) (resp. PMM (𝒦, 𝒫)).


4. Equilibrium Description Logics
Following [7], we recall Equilibrium Description Logics (EDLs), i.e. DLs under the stable model semantics
of Quantified Equilibrium Logic. Equilibrium Logic (EL) [14] is a powerful formalism that allows, e.g.,
extending the stable model semantics of Answer Set Programming (ASP) to arbitrary theories. EL is built
upon the logic of Here-and-There (HT) with an additional minimality requirement and its first-order
counterpart, Quantified Equilibrium Logic (QEL), has been introduced in [9]. An interpretation in the
HT logic consists of a pair of structures (ℐ, 𝒥 ) sharing the same domain and interpreting individuals in
the same way, where ℐ is called ‘here’ interpretation and 𝒥 is called ‘there’ interpretation. Intuitively
speaking, the ‘here’ interpretation corresponds to a world (in the sense of Kripke frames) where the
truth of an atom can be seen as a belief. While the ‘there’ world corresponds to what is assumed to be
possible. These two interpretations are related by the inclusion relation, intuitively corresponding to the
fact that only possible facts can be believed. We formalize this requirement by recalling the relations
⊆𝐹 and ⊂𝐹 of Definition 2 where the set of fixed predicates 𝐹 ⊆ NC ∪ NR specifies those predicates
over which the ‘here’ and the ‘there’ interpretations must agree.

Definition 7. A Here-and-There (HT) interpretation is a pair (ℐ, 𝒥 ) of interpretations with ℐ ⊆𝐹 𝒥 ,
with 𝐹 ⊆ NC ∪ NR . The interpretation function ·(ℐ,𝒥 ) is defined in Figure 1.

   In general, under the HT semantics predicates do not obey the law of the excluded middle. Already
in the case of propositional HT logic, the formula 𝑥 ∨ ¬𝑥 is not a tautology [8]. Given an HT inter-
pretation (ℐ, 𝒥 ) as in Definition 7, we can refer to the predicates in the 𝐹 as classical: indeed since
the interpretations ℐ and 𝒥 agree on the extension of predicates in 𝐹 , the law of the excluded middle
applies for each 𝑝 ∈ 𝐹 .
   As already pointed out in [7], 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. Indeed, in HT logic – whether quantified or not – the implication is intuitionistic
[8, 9] and it is true in an HT interpretation when the following are satisfied: (1) if the antecedent is
true in the HT interpretation, then the consequence is true in the HT interpretation, and (2) the ‘there’
interpretation is a classical model of it. As a matter of fact, concept inclusions are also affected by this
double nature of implication, as they are ‘explicit’ implications in DLs.

Definition 8. Assume a KB 𝒦 = (𝒯 , 𝒜) and an HT interpretation (ℐ, 𝒥 ). We write:

- (ℐ, 𝒥 ) |= 𝐶 ⊑ 𝐷, if 𝐶 (ℐ,𝒥 ) ⊆ 𝐷(ℐ,𝒥 ) and 𝐶 𝒥 ⊆ 𝐷𝒥 ;

- (ℐ, 𝒥 ) |= 𝒦 if ℐ |= 𝒜 and (ℐ, 𝒥 ) |= 𝐶 ⊑ 𝐷 for all 𝐶 ⊑ 𝐷 ∈ 𝒯 .

  We can now define stable models of a DL KB.

Definition 9 (Stable models). 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 ℐ ⊂𝐹 𝒥 .

We denote with SM 𝐹 (𝒦) the set of all stable models for 𝒦 with fixed predicates 𝐹 . If 𝐹 = ∅, we drop the
subscript 𝐹 and write SM (𝒦).

   Similarly to the approach of this paper, in the stable model semantics of [15], the set of predicates is
partitioned in intentional predicates – subjected to the minimization, and extensional predicates – which
are classical and thus obey the law of the excluded middle. The latter requirement, in the setting of full
first-order logic, can be easily expressed with the conjunct 𝑝 ∨ ¬𝑝, for each extensional predicate 𝑝.
However, in the setting of the DLs considered in this work, we can express fixed concept names but not
fixed roles. This is not a limit, as we already parametrized the relation ⊆𝐹 expressing the predicates
that are fixed.
   In the semantics given in Definition 9, the negation ¬ behaves as negation as failure or default
negation in logic programs: the truth of a negated concept ¬𝐶 at a certain domain element in a stable
model intuitively means that the concept 𝐶 could not be proved at such domain element. As already
underlined in [7], the fact that negation is not anymore classical implies that KBs that are equivalent
under the classical semantics might not be equivalent under the stable model semantics.
Example 1 (From [6]). Assume that we want to describe the following scenario. Administrators can grant
access to classified files. If a classified file is read, the permission to do so should have been granted. Consider
the knowledge base 𝒦

                    Classified_Document(𝑓1 )         User(𝐽𝑜ℎ𝑛)       read(𝐽𝑜ℎ𝑛, 𝑓1 )
                    ∃access_granted_by.Admin ⊑ Has_Read_Permission
                    Classified_Document ⊓ ¬∀(read)− .Has_Read_Permission ⊑ ⊥

Assume that Admin and access_granted_by are fixed predicates. We derive that all classified documents
must be read by someone who has permission to do so. As an effect of ‘¬’ behaving as default negation,
such permission is not ‘justified’ by the last inclusion above and must come from an Admin. Thus, in every
stable model, we derive that John, who is reading the classified document 𝑓1 , has permission granted by an
admin.

   In Definition 4 we introduce a relation comparing interpretations that differ only at a single domain
element, in terms of concept names and role names involving it. We lift this pointwise comparison to
defining pointwise stable models as follows. Recall the definition of ⊆∙𝐹 and ⊂∙𝐹 .

Definition 10 (Pointwise Stable Models). Given 𝐹 ⊆ 𝑁𝐶 ∪ 𝑁𝑅 , an interpretation 𝒥 is a pointwise
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 ℐ ⊂∙𝐹 𝒥 .

We denote with PSM 𝐹 (𝒦) the set of all stable models for 𝒦 with fixed predicates 𝐹 . If 𝐹 = ∅, we drop
the subscript 𝐹 and write PSM (𝒦).

   Remark. Pointwise stable models have been already considered for full first-order logic in [15].
However, there are some key differences with the above definition. Ferraris et al. achieve the stable model
semantics by means of an operator associating each first-order formula Φ to a second-order formula
SM [Φ] whose models are stable. In the case of pointwise circumscription, the operator associates the
formula PSM [Φ] which can be expressed at the first-order level. The performed pointwise minimization
in PSM [Φ] allows only for the minimization of a single predicate. In our setting, multiple predicates
with multiple arities can be minimized, as long as they ‘concern’ a unique domain element.
  The reasoning tasks of concept satisfiability, subsumption and instance checking can be adapted in the
usual way to stable models and pointwise stable models.
  We strengthen the undecidability result for 𝒜ℒ𝒞ℐ of [7] showing that concept satisfiability is
undecidable in 𝒜ℒ𝒞 under the stable model semantics via a reduction from the domino problem.

Theorem 1. Concept satisfiability w.r.t general KBs in 𝒜ℒ𝒞 under the stable model semantics is undecid-
able.

   In [6], concept satisfiability is proved to be undecidable w.r.t general KBs in 𝒜ℒ𝒞ℐ𝒪 under pointwise
circumscription. The result is obtained via a reduction from the domino problem and the constructed
TBox is negation-free. As already proved in [7], for negation-free KBs, minimal models coincide with
stable models. The same holds if we restrict to pointwise minimal models and pointwise stable models.
Since nominals can be simulated in the pointwise stable model semantics using default negation as
done in [7], the following result follows.

Theorem 2. Concept satisfiability w.r.t general KBs in 𝒜ℒ𝒞ℐ under the pointwise stable model semantics
is undecidable.
5. Constrained Circumscription
In order to characterize the connection of EDL KBs and circumscribed KBs, we extend circumscription
with constraints. The notion of constraints has been introduced in [6] for pointwise circumscribed KBs
as a tool for normalizing complex concepts without affecting minimization. A constraint in the sense
of [6] is a pair (𝐶, 𝐷) with the intuitive meaning “if 𝐶 holds, then 𝐷 must hold too”. Coupled with a
circumscribed (or pointwise circumscribed) KB, constraints allow for further refinement of the set of
minimal models, as the requirement expressed by constraints acts outside circumscription. As one can
observe, a constraint is nothing but a GCI. In this work, we extend the notion of constraints of [6] to
KBs as follows.

Definition 11. Assume two KBs 𝒦 and 𝒞 equipped with a circumscription pattern 𝒫. Given an interpreta-
tion ℐ, we say that ℐ is a (pointwise) minimal model of Circ𝒫 (𝒦) ∧ 𝒞, in symbols ℐ |=(∙) Circ𝒫 (𝒦) ∧ 𝒞,
if ℐ |=(∙) Circ𝒫 (𝒦) and ℐ |= 𝒞. We call constraint set the KB 𝒞 .

   Compared to [6] where constraints were restricted to mimicking concept inclusions, we not only
allow assertions in the constraints but also role inclusions. Furthermore, we remark that the two KBs 𝒦
and 𝒞 can share the signature.

Example 2. Recall the KB 𝒦 of Example 1. Let us consider 𝒦′ ⊆ 𝒦 given by and circumscribed with
𝑀 = {Has_Read_permission} and keeping all the other predicates fixed. Consider the constraint set
𝒞 = {Classified_Document ⊑ ∀(read)− .Has_Read_Permission}. As in Example 1, the inclusion above
imposes that whenever a classified document is read, the user reading it has permission to do so. Since the
predicate Has_Read_Permission is minimized, in minimal models of 𝒦′ , any permission must be granted
by an Admin. Applying Definition 11, we find that in every minimal model ℐ of Circ𝒫 (𝒦′ ) ∧ 𝒞, John
got the reading permission from an Admin. Counterintuitively, if we push the constraint set 𝒞 inside the
circumscription, i.e. we look for minimal models of Circ𝒫 (𝒦′ ∪ 𝒞) we can derive that John has permission
to read 𝑓1 without the approval of an administrator.

   Following [1], we can prove that the standard filtration technique (see [12]) can be used to show that
circumscribed 𝒜ℒ𝒞ℋℐ𝒪 with constraints has the ‘small’ (exponential size) model property under the
assumption that roles are varying. The latter result yields the following.

Theorem 3. Concept satisfiability in circumscribed 𝒜ℒ𝒞ℋℐ𝒪 with constraints is NExpTimeNP -complete
if all roles are varying.

   Filtration has been used in [2] for showing that circumscribed DL-Liteℋ 𝐵𝑜𝑜𝑙 has the small model
property under the condition that no varying role is subsumed by a fixed role. A KB in DL-Liteℋ 𝐵𝑜𝑜𝑙
that satisfies this condition is called role-layered. The model construction is the same applied for
circumscribed 𝒜ℒ𝒞ℋℐ𝒪 with varying roles, however, the restricted syntax of DL-Lite𝐵𝑜𝑜𝑙 allows for
handling the presence of fixed roles too. The upper bound of Theorem 3 applies also if role-layered
circumscribed KBs in DL-Liteℋ  𝐵𝑜𝑜𝑙 are paired with constraints in 𝒜ℒ𝒞ℋℐ𝒪.

Corollary 1. Concept satisfiability in role-layered circumscribed DL-Liteℋ
                                                                         𝐵𝑜𝑜𝑙 with constraints in
𝒜ℒ𝒞ℋℐ𝒪 is in NExpTimeNP .

Expressing Closed Predicates. In DLs with closed predicates [16, 17], the extension of some
predicates – so-called closed – is restricted only to named individuals whose participation in the closed
predicates is ‘justified’ by ABox assertions. An interpretation is a model of a KB 𝒦 = (𝒜, 𝒯 ) w.r.t. a set
Σ of closed predicates, in symbols ℐ |= (𝒜, 𝒯 , Σ), if ℐ |= 𝒦 and for each 𝐴, 𝑟 ∈ Σ:

    • 𝑑 ∈ 𝐴ℐ implies 𝑑 = 𝑎ℐ for some individual 𝑎 such that 𝐴(𝑎) ∈ 𝒜, and

    • (𝑑, 𝑒) ∈ 𝑟ℐ implies 𝑑 = 𝑎ℐ and 𝑒 = 𝑏ℐ with 𝑎, 𝑏 such that 𝑟(𝑎, 𝑏) ∈ 𝒜.
Intuitively speaking, the extension of a closed predicate 𝑝 is ‘circumscribed’ to instances of 𝑝 given by
ABox assertions. Although the underlying principle is close to predicate minimization, DLs with closed
predicates and (pointwise) circumscribed DLs are two different non-monotonic formalisms and we see
no obvious formal translation. On the other hand, constrained circumscription can easily capture DLs
with close predicates.
   Given a KB 𝒦 = (𝒜, 𝒯 ) with a set of closed predicates Σ, let Σ′ = {𝑝′ | 𝑝 ∈ Σ}, i.e. we consider
a copy of the signature in Σ. Let 𝒜′ = {𝑝′ (𝑐           ⃗) ∈ 𝒜 and 𝑝 ∈ Σ}. We obtain this way a new KB
                                                 ⃗) | 𝑝(𝑐
𝒦′ = (𝒜 ∪ 𝒜′ , 𝒯 ). We now define a circumscription pattern 𝒫 for 𝒦′ by stating that all predicates in
Σ′ are minimized. Since 𝒯 does not contain any occurrence of symbols in Σ′ , in a minimal model ℐ ′
we will have that each 𝑝′ ∈ Σ′ contains only named individuals or pairs of named individuals, whose
participation in (𝑝′ )ℐ is justified by an assertion in 𝒜′ . To the circumscribed KB Circ𝒫 (𝒦′ ), we add the
set of constraints 𝒞 = {𝑝 ⊑ 𝑝′ | 𝑝 ∈ Σ}. In every model ℐ of Circ𝒫 (𝒦′ ) ∧ 𝒞, every element of 𝑝ℐ is an
element of (𝑝′ )ℐ . In this way, we force 𝑝 to be closed.

Theorem 4. Concept satisfiability w.r.t KBs with closed predicates can be polynomially reduced to concept
satisfiability w.r.t. (pointwise) circumscribed KBs with constraints.

   The result above almost directly implies that nominals can be simulated using constraints. Indeed this
is already possible via closed predicates: each nominal 𝑜 can be simulated by replacing every occurrence
of 𝑜 with a closed predicate 𝑁 and adding an assertion 𝑁 (𝑜). A similar idea has been used in [7] to
show that nominals can be simulated in EDLs.


6. From EDLs to Circumscribed DLs with Constraints
Given a KB 𝒦 and a set 𝐹 of fixed predicates, we aim to build a KB 𝒦   ¯ with a circumscription pattern 𝒫
and a set of constraints 𝒞 such that there is a correspondence between stable models of 𝒦 and model of
Circ𝒫 (𝒦 ¯ ) ∧ 𝒞 up to the original signature. We give a sketch of the translation that we adapted from
[18].
    The first step of our construction is to simulate HT interpretations. We consider a copy Σ′ of the
signature Σ of 𝒦, which we use to split the ‘here’ and the ‘there’ interpretations. Intuitively speaking,
the interpretation of primed predicates corresponds to the interpretations of predicates in the ‘there’
interpretation. We construct the KB 𝒦   ¯ taking the union of two KBs 𝒦′ and 𝒦⋆ . The KB 𝒦′ is obtained
from 𝒦 by replacing each symbol with its primed counterpart. We use 𝒦′ to require that the ‘there’ is a
classical model of 𝒦. The KB 𝒦⋆ is obtained by replacing each concept 𝐶 occurring negatively in 𝒦
with 𝐶 ′ . This second KB is used to simulate the interpretation of negated concepts in the HT semantics
(see Figure 1).
    To capture the stable model semantics in the setting of circumscription, we require that all predicates
in the original signature of 𝒦 are minimized while all primed predicates are fixed. To synchronize the
‘here’ and the ‘there’, ensuring that the interpretations of primed and non-primed symbols coincide, we
introduce constraints of the form 𝑃 ⊑ 𝑃 ′ and 𝑃 ′ ⊑ 𝑃 , for each predicate symbol 𝑃 . These constraints
filter out minimal models that are not stable.
    A natural question is: do we really need to rely on constrained circumscription? Circumscription and
Equilibrium Logic are two orthogonal formalisms, as already argued in [15].

Example 3. Consider the TBox 𝒯 = {¬𝐴 ⊑ 𝐴} with 𝐹 = ∅. It is easy to show that 𝒯 has no stable
model. Indeed, given ℐ such that Δℐ = {𝑥} and ℐ |= 𝒯 , then 𝐴ℐ = {𝑥}. The interpretation 𝒥 such
that Δ𝒥 = Δℐ and 𝐴𝒥 = ∅ is such that (𝒥 , ℐ) |= 𝒯 . If we apply (pointwise) circumscription, the most
natural option to ‘mimic’ the stable model semantics is to minimize 𝐴. One can observe that the previous
model ℐ of 𝒯 is minimal.

Example 4. Consider the TBox 𝒯 = {𝐵 ⊑ 𝐴 ⊔ ¬𝐴} and assume 𝐹 = {𝐵}. We can show that 𝐴 is
satisfiable in a stable model of 𝒯 . Indeed, the interpretation ℐ such that Δℐ = {𝑥}, 𝐵 ℐ = 𝐴ℐ = {𝑥} is a
stable model 𝒯 such that 𝐴ℐ = ∅. If one considers now (pointwise) circumscription, as before a natural
direction is to respect the ‘nature’ of predicates, i.e. keep 𝐵 fixed and minimize 𝐴. However, assuming that
𝐴 is minimized, it is straightforward to see that there is no minimal model 𝒥 of 𝒯 such that 𝐴𝒥 ̸= ∅.

The transformation. Given a KB 𝒦 = (𝒜, 𝒯 ), let Σ denote the set of all concept names and role
names occurring in 𝒦. We consider a copy of the signature Σ and we denote it with Σ′ = {𝐴′ |𝐴 ∈
𝐴} ∪ {𝑟′ |𝑟 ∈ Σ}. Given a complex concept 𝐶 we denote with 𝐶 ′ the concept over Σ′ obtained globally
replacing each predicate symbol in 𝐶 with its primed version. Following [18], we define an operator 𝜏
recursively as follows:
    • 𝜏 (𝐴) = 𝐴, 𝜏 (𝑟) = 𝑟, 𝜏 (⊤) = ⊤, 𝜏 (⊥) = ⊥, 𝜏 ({𝑎}) = {𝑎},

    • 𝜏 (¬𝐶) = ¬𝐶 ′ , 𝜏 (∃𝑅.𝐶) = ∃𝑅.𝜏 (𝐶) and 𝜏 (∀𝑅.𝐶) = ∀𝑅.𝜏 (𝐶) ⊓ ∀𝑅′ .𝐶 ′

    • 𝜏 (𝐶 ∘ 𝐷) = 𝜏 (𝐶) ∘ 𝜏 (𝐷), with ∘ ∈ {⊓, ⊔}.
Given the TBox 𝒯 , we denote with 𝒯 * the resulting TBox, with predicates occurring in Σ ∪ Σ′ , obtained
applying 𝜏 to all GCIs in 𝒯 , i.e. 𝒯 ⋆ = {𝜏 (𝐶) ⊑ 𝜏 (𝐷)|𝐶 ⊑ 𝐷 ∈ 𝒯 }. Observe that the assertions in the
ABox can be seen as inclusions in the standard way. It is easy to observe that they are not affected by
the 𝜏 transformation. We 𝒦⋆ = (𝒜, 𝒯 ⋆ ). We denote with 𝒦′ the KB obtained from 𝒦 by replacing each
symbol 𝑝 ∈ Σ with its primed counterpart 𝑝′ ∈ Σ′ .
   Given a set Σ of concept names and role names and interpretation 𝒥 , we denote with 𝒥 ′ the
                                       ′      ′
interpretation such that Δ𝒥 = Δ𝒥 , (𝑝′ )𝒥 = 𝑝𝒥 for all 𝑃 ∈ Σ. Given an HT interpretation (ℐ, 𝒥 ),
                                                            ′                    ′
we denote with ℐ ∪ 𝒥 ′ the interpretation such that Δℐ∪𝒥 = Δℐ = Δ𝒥 , 𝑃 ℐ∪𝒥 = 𝑃 ℐ for all 𝑃 ∈ Σ
             ′
and (𝑃 ′ )ℐ∪𝒥 = 𝑃 𝒥 for all 𝑃 ′ ∈ Σ′ .
   As mentioned at the beginning of this section, we aim to simulate the HT semantics. Roughly
speaking, given an HT interpretation, we copy the ‘there’ interpretation using the primed symbols,
while unprimed symbols are interpreted as in the ‘here’.
Lemma 1. Assume a KB 𝒦 and two interpretations ℐ and 𝒥 . Let Σ be the set of predicates occurring in 𝒦
and 𝐹 ⊆ Σ be a set of fixed predicates. Then (ℐ, 𝒥 ) is a HT model of 𝒦 with fixed predicates in 𝐹 if and
only if ℐ ∪ 𝒥 ′ is a model of 𝒦* ∪ 𝒦′ ∪ {𝑝 ⊑ 𝑝′ ∈ Σ} ∪ {𝑝′ ⊑ 𝑝|𝑝 ∈ 𝐹 }.
   We now use circumscription to capture stable models. With the following theorem, we formalize the
intuitive explanation given at the beginning of this section.
Theorem 5. Assume a KB 𝒦 = (𝒜, 𝒯 ) and an interpretation ℐ. Let Σ be the set of predicates occurring
in 𝒦 and 𝐹 ⊆ Σ, ℐ ∈ SM 𝐹 (𝒦) if and only if ℐ ∪ ℐ ′ is a model of Circ𝒫𝐹 (𝒦* ∪ 𝒦′ ) ∧ 𝒞, with
𝒞 = {𝑝 ⊑ 𝑝′ , 𝑝′ ⊑ 𝑝|𝑝 ∈ Σ} and 𝒫𝐹 = (𝑀, ∅, 𝐹 ∪ Σ′ ) with 𝑀 = Σ ∖ 𝐹 .
   Since 𝒦′ contains only fixed predicates, alternatively we can add it to the set of constraints. Theorem
5 extends to the case of pointwise EDLs and pointwise circumscribed DLs with constraints.
Theorem 6. Assume a KB 𝒦 = (𝒜, 𝒯 ) and an interpretation ℐ. Let Σ be the set of predicates occurring
in 𝒦 and 𝐹 ⊆ Σ, ℐ ∈ PSM 𝐹 (𝒦) if and only if ℐ ∪ ℐ ′ is a model of Circ∙𝒫𝐹 (𝒦* ∪ 𝒦′ ) ∧ 𝒞, with
𝒞 = {𝑝 ⊑ 𝑝′ , 𝑝′ ⊑ 𝑝|𝑝 ∈ Σ} and 𝒫𝐹 = (𝑀, ∅, 𝐹 ∪ Σ′ ) with 𝑀 = Σ ∖ 𝐹 .


7. Conclusions
In this paper, we established a translation from Equilibrium DLs (EDLs) and circumscribed DLs with
constraints, both under global and pointwise minimization. These two formalisms are interesting on
their own and understanding the complexity of one can help in understanding the complexity of the
other. Therefore, our future research will follow two main lines. We plan to investigate the expressive
power and the computational complexity of EDLs. In particular, we aim to focus on lightweight EDLs
in the DL-Lite family. Via the translation of EDLs into circumscribed DLs with constraints, we can
refine our investigation by studying the complexity of reasoning in circumscribed DLs with constraints.
The preliminary results presented in this paper involve varying predicates, that are not supported in
EDLs. We are also interested in identifying syntactic restrictions under which global and pointwise
circumscription (with constraints) coincide, inheriting the good computational properties of the latter
for both EDLs and pointwise EDLs. Furthermore, we aim to explore the connection between EDLs and
DLs based on MKNF [19], and fuzzy DLs under the (3-valued) Gödel semantics [20].


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. A part of this research was done when Mantas Šimkus was employed at Umeå
University, Sweden.


References
 [1] P. A. Bonatti, C. Lutz, F. Wolter, The complexity of circumscription in description logic, J. Artif.
     Intell. Res. 35 (2009) 717–773.
 [2] P. A. Bonatti, M. Faella, C. Lutz, L. Sauro, F. Wolter, Decidability of circumscribed description
     logics revisited, in: Advances in Knowledge Representation, Logic Programming, and Abstract
     Argumentation, volume 9060 of Lecture Notes in Computer Science, Springer, 2015, pp. 112–124.
 [3] P. A. Bonatti, F. Di Stefano, M. Ortiz, M. Simkus, Circumscription in DL-Lite: Progress report, in:
     Description Logics, volume 3515 of CEUR Workshop Proceedings, CEUR-WS.org, 2023.
 [4] C. Lutz, Q. Manière, R. Nolte, Querying circumscribed description logic knowledge bases, in: KR,
     2023, pp. 482–491.
 [5] P. A. Bonatti, M. Faella, L. Sauro, Defeasible inclusions in low-complexity DLs, J. Artif. Intell. Res.
     42 (2011) 719–764.
 [6] F. Di Stefano, M. Ortiz, M. Šimkus, Description logics with pointwise circumscription, in: Proc. of
     IJCAI 2023, ijcai.org, 2023, pp. 3167–3175.
 [7] F. Di Stefano, M. Simkus, Stable model semantics for description logic terminologies, in: Proc. of
     AAAI 2024, AAAI, 2024, pp. 10484–10492.
 [8] D. Pearce, Equilibrium logic, Ann. Math. Artif. Intell. 47 (2006) 3–41.
 [9] 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.
[10] 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.
[11] G. De Giacomo, M. Lenzerini, A uniform framework for concept definitions in description logics,
     J. Artif. Intell. Res. 6 (1997) 87–110.
[12] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
     University Press, 2017.
[13] V. Lifschitz, Pointwise circumscription: Preliminary report, in: Proc. of AAAI 1986, Morgan
     Kaufmann, 1986, pp. 406–410.
[14] D. Pearce, A new logical characterisation of stable models and answer sets, in: NMELP, volume
     1216 of Lecture Notes in Computer Science, Springer, 1996, pp. 57–70.
[15] P. Ferraris, J. Lee, V. Lifschitz, Stable models and circumscription, Artif. Intell. 175 (2011) 236–263.
[16] E. Franconi, Y. A. Ibáñez-García, İnanç Seylan, Query answering with DBoxes is hard, Electronic
     Notes in Theoretical Computer Science 278 (2011) 71–84. Proceedings of the 7th Workshop on
     Methods for Modalities (M4M’2011) and the 4th Workshop on Logical Aspects of Multi-Agent
     Systems (LAMAS’2011).
[17] C. Lutz, I. Seylan, F. Wolter, Ontology-based data access with closed predicates is inherently
     intractable(sometimes), in: Proc. of IJCAI 2013, IJCAI/AAAI, 2013, pp. 1024–1030.
[18] D. Pearce, H. Tompits, S. Woltran, Characterising equilibrium logic and nested logic programs:
     Reductions and complexity, , Theory Pract. Log. Program. 9 (2009) 565–616.
[19] F. M. Donini, D. Nardi, R. Rosati, Description logics of minimal knowledge and negation as failure,
     ACM Trans. Comput. Log. 3 (2002) 177–225.
[20] F. Bobillo, M. Delgado, J. Gómez-Romero, U. Straccia, Fuzzy description logics under Gödel
     semantics, International Journal of Approximate Reasoning 50 (2009) 494–514. Special Section on
     Bayesian Modelling.

</pre>