=Paper=
{{Paper
|id=Vol-3263/paper-7
|storemode=property
|title=Pointwise Circumscription in Description Logics
|pdfUrl=https://ceur-ws.org/Vol-3263/paper-7.pdf
|volume=Vol-3263
|authors=Federica Di Stefano,Magdalena Ortiz,Mantas Simkus
|dblpUrl=https://dblp.org/rec/conf/dlog/Stefano0S22
}}
==Pointwise Circumscription in Description Logics==
<pdf width="1500px">https://ceur-ws.org/Vol-3263/paper-7.pdf</pdf>
<pre>
Pointwise Circumscription in Description Logics
Federica Di Stefano1 , Magdalena Ortiz1 and Mantas Šimkus1,2
1
    Institute of Logic and Computation, TU Wien, Austria
2
    Department of Computing Science, Umeå University, Sweden


                                         Abstract
                                         Circumscription is one of the major approaches to bring non-monotonic (common-sense) reasoning
                                         features to first-order logic and related formalisms, and it has already received attention in Description
                                         Logics (DLs), with the focus on understanding the computational complexity of reasoning. Those studies
                                         revealed that circumscription causes a dramatic increase in computational complexity in a broad range
                                         of DLs. In this paper, we consider a new notion of circumscription in DLs, aiming to preserve the key
                                         ideas and advantages of classical circumscription while mitigating its impact on the computational
                                         complexity of reasoning. Our main idea is to replace the second-order quantification step with a series
                                         of (pointwise) local checks on all domain elements and their immediate neighborhood. This approach
                                         provides a sound approximation of classical circumscription and is closely related to the notion of
                                         pointwise circumscription proposed by Lifschitz for first-order logic. Our main achievement is to show
                                         that, under certain syntactic restrictions, standard reasoning problems like subsumption testing or
                                         concept satisfiability for 𝒜ℒ𝒞ℐ𝒪 KBs with pointwise circumscription are (co)NExpTime-complete.




1. Introduction
As fragments of first-order logic, Description Logics (DLs) inherit many of its features, including
monotonicity. In a monotonic logic, adding new knowledge to a knowledge base does not
invalidate the previously derived knowledge. Humans in their everyday life often resort to non-
monotonic reasoning, e.g., when dealing with incomplete information. Adding non-monotonic
features to monotonic formalisms is a big challenge, and it often causes undecidability or a
significant increase in the complexity of reasoning. Several non-monotonic extensions of DLs
have been proposed, aiming to balance the computational cost and the expressiveness (see, e.g.,
[1, 2, 3, 4]). A prominent research line here is circumscribed DLs [5, 6, 7, 4]. Circumscription
is a powerful tool that was first introduced by McCarthy as an extension of first-order logic.
In its basic form, the intended (or preferred) models of a circumscribed theory are obtained by
considering its classical models and additionally minimizing the extensions of some selected
predicates [8, 9, 10]. In general, additionally to the predicates to be minimized, one may specify—
by means of a circumscription pattern—the predicates whose extensions must remain fixed and
the predicates that may vary freely. Circumscription in DLs has different expressiveness benefits,
but unfortunately the complexity of reasoning in circumscribed DLs is often very high, and
undecidability is easily encountered [11, 4]. The key reason for the high complexity is the second-
order quantification that is needed in order to identify the preferred models of a circumscribed

  DL 2022: 35th International Workshop on Description Logics, August 7–10, 2022, Haifa, Israel
" federica.stefano@tuwien.ac.at (F. Di Stefano); ortiz@kr.tuwien.ac.at (M. Ortiz); simkus@cs.umu.se (M. Šimkus)
                                       © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)
DL knowledge base (KB). The main goal of our work is to lower the computational complexity
of reasoning by considering an alternative (weaker) notion of circumscription that is useful for
knowledge representation and does not use such a powerful second-order quantification.
   We introduce pointwise circumscription in DLs. The basic idea here is to replace the single
global minimality check of classic circumscription by multiple local minimality checks at all
domain elements and their immediate neighborhood. Since the local minimality checks of
pointwise circumscription are not capable of detecting self-justification cycles that span two
or more domain elements—something easily detectable using second-order quantification of
classic circumscription—pointwise circumscription is strictly weaker than (and it thus provides
a sound approximation of inferences w.r.t. ) classic circumscription. That is, given a KB and a
circumscription pattern, the preferred models under pointwise circumscription will subsume
the preferred models under classic circumscription, but not necessarily the other way around.
   The term “pointwise circumscription” was coined by Lifschitz in [12] for full first-order
logic, where the second-order quantification over predicate extensions is replaced with a
series of individual additions or removals of tuples (points) in predicates, performed point-
wise. To get some intuition behind this, consider a theory 𝜙 consisting of the single formula
(∃𝑥, 𝑦.𝐴(𝑥, 𝑦)) ∧ (∀𝑥, 𝑦.𝐴(𝑥, 𝑦) ↔ (𝐵(𝑦, 𝑥) ∨ 𝐶(𝑦, 𝑥)) and suppose we want all predicates
𝐴, 𝐵, 𝐶 to be minimized. Consider three models of 𝜙 over the domain {𝑐, 𝑑} represented in the
obvious way as sets of atoms 𝐼1 = {𝐴(𝑐, 𝑑), 𝐵(𝑑, 𝑐)}, 𝐼2 = {𝐴(𝑐, 𝑑), 𝐵(𝑑, 𝑐), 𝐴(𝑑, 𝑐), 𝐵(𝑐, 𝑑)},
𝐼3 = {𝐴(𝑐, 𝑑), 𝐵(𝑑, 𝑐), 𝐴(𝑑, 𝑐), 𝐵(𝑐, 𝑑), 𝐶(𝑐, 𝑑)}. To check whether a structure above is an
intended model according to Lifschitz’s pointwise (resp., classic) circumscription we need to
see if we can remove one atom (resp., a set of atoms) such that the resulting structure remains
a model of 𝜙. Observe that given 𝐼1 or 𝐼2 , we cannot obtain a new model of 𝜙 by deleting
a single atom from them thus 𝐼1 , 𝐼2 are both minimal models of 𝜙 in the sense of pointwise
circumscription. However, 𝐼2 is not a minimal model in the sense of classic circumscription,
because by deleting the pair 𝐴(𝑑, 𝑐), 𝐵(𝑐, 𝑑) from 𝐼2 we obtain a model of 𝜙. 𝐼1 is clearly an
intended model under classic circumscription. 𝐼3 is not an intended model under either notions
of circumscription because the deletion of 𝐶(𝑐, 𝑑) still leads to a model of 𝜙. Observe that
pointwise circumscription did not eliminate 𝐼2 because it did not identify a self-justification
cycle: 𝐴(𝑑, 𝑐) survives in 𝐼2 because of the presence of 𝐵(𝑐, 𝑑), and 𝐵(𝑐, 𝑑) survives because
of the presence of 𝐴(𝑑, 𝑐). The variant of circumscription we consider in this paper is closely
related in spirit but is technically orthogonal to the one of Lifschitz. We consider a restricted
fragment of first-order logic (concretely, the DL 𝒜ℒ𝒞ℐ𝒪) and perform a single model “improve-
ment” step that allows to modify the configuration of a domain element, i.e., its membership in
concept names and roles.
   The main contributions of this paper are the following.
    • We define the framework of pointwise circumscription in DLs. To do this, we introduce a
      simple notion of comparability relations for pairs of interpretations, which allows defining
      different variants of pointwise circumscription. These variants correspond to different
      ways we are allowed to make local improvements to a given model of a DL KB. For further
      study, we settle on a “star-based” variant where at each domain object 𝑒 we are allowed
      to simultaneously change the participation of the object 𝑒 in concept names and roles.
    • We provide a method for reasoning under pointwise circumscription in TBoxes in the
      very expressive DL 𝒜ℒ𝒞ℐ𝒪. The reasoning tasks include concept satisfiability, concept
      subsumption, and entailment of assertions. In this preliminary work, we consider TBoxes
      with inclusions of a specific shape, similar to various ‘normalized’ TBoxes in the literature,
      and where concept expressions are limited to modal depth 1. We show that in this setting,
      reasoning is feasible in (co)NExpTime. The upper bounds are obtained by applying the
      mosaic technique and integer programming. The basic idea of the mosaic technique [13]
      is that showing the existence of a model is equivalent to showing the existence of a set of
      fragments of models. We call these fragments star types. We define a minimality condition
      over star types and following the work done in [14] and [15], we provide algorithms by
      means of integer programming.

    • We show that satisfiability of concept names in pointwise circumscribed 𝒜ℒ𝒞ℐ𝒪 TBoxes
      in our restricted form is already hard for NExpTime. This is done by providing a reduction
      from the tiling problem for exponential grids, and it shows that the upper bounds of this
      paper are worst-case optimal.


2. Preliminaries
We denote with 𝑁𝐶 , 𝑁𝑅 , and 𝑁𝐼 countably infinite sets of concept names (unary predicates),
role names (binary predicates), and individual names (constants). The inverse role of a role name
𝑟 ∈ 𝑁𝑅 is 𝑟− . We define the set of roles 𝑁𝑅+ = 𝑁𝑅 ∪ {𝑟− | 𝑟 ∈ 𝑁𝑅 }. We let 𝑟−− = 𝑟, and given
a set 𝑅 of roles, we define 𝑅− = {𝑟− | 𝑟 ∈ 𝑅}. In 𝒜ℒ𝒞ℐ𝒪, concepts are defined according to the
syntax 𝐶 := ⊤| ⊥| 𝐴| {𝑎}| ¬𝐶| 𝐶 ⊔ 𝐶| 𝐶 ⊓ 𝐶| ∃𝑟.𝐶| ∀𝑟.𝐶, with 𝐴 ∈ 𝑁𝐶 , 𝑟 ∈ 𝑁𝑅+ , and 𝑎 ∈ 𝑁𝐼 .
An expression of the form 𝐶 ⊑ 𝐷, with 𝐶 and 𝐷 concepts, is a concept inclusion. An expression
of the form 𝐴(𝑎), where 𝐴 ∈ 𝑁𝐶 and 𝑎 ∈ 𝑁𝐼 , is a concept assertion. An expression of the form
𝑟(𝑎, 𝑏), with 𝑟 ∈ 𝑁𝑅 and 𝑎, 𝑏 ∈ 𝑁𝐼 , is a role assertion. A TBox 𝒯 in 𝒜ℒ𝒞ℐ𝒪 is a collection of
concept inclusions, and an ABox 𝒜 is a collection of concept and role assertions. A knowledge
base 𝒦 in 𝒜ℒ𝒞ℐ𝒪 is a pair (𝒯 , 𝒜), with 𝒯 a TBox and 𝒜 an ABox. Given a TBox, we denote
with 𝑁𝐶 (𝒯 ), 𝑁𝑅 (𝒯 ), and 𝑁𝐼 (𝒯 ) the sets of concept names, role names, and individual names
occurring in 𝒯 . We denote with 𝑁𝐶+ = 𝑁𝐶 ∪ {{𝑎}| 𝑎 ∈ 𝑁𝐼 } ∪ {⊤, ⊥} the set of basic concepts.
Given a TBox 𝒯 , 𝑁𝐶+ (𝒯 ) denotes the set of basic concepts occurring in 𝒯 and 𝑁𝑅+ (𝒯 ) the set
of roles occurring in 𝒯 . The semantics is defined by means of interpretations ℐ = (Δℐ , ·ℐ ). The
two components Δℐ and ·ℐ are called domain and interpretation function. The latter associates
to each 𝑎 ∈ 𝑁𝐼 a unique element in the domain, to each 𝐴 ∈ 𝑁𝐶 a set 𝐴ℐ ⊆ Δℐ and to each
𝑟 ∈ 𝑁𝑅 a set 𝑟ℐ ⊆ Δℐ × Δℐ . The semantics for 𝒜ℒ𝒞ℐ𝒪 concepts is defined as usual [16].
The notions of model of an inclusion, a TBox, a KB are also standard. Given an interpretation
ℐ = (Δℐ , ·ℐ ), for any 𝑑 ∈ Δℐ , we define the unary type of 𝑑 as 𝑢𝑡ℐ (𝑑) = {𝐴 ∈ 𝑁𝐶+ | 𝑑 ∈ 𝐴ℐ },
and for any 𝑒 ∈ Δℐ , we define the binary type of (𝑑, 𝑒) as 𝑏𝑡ℐ (𝑑, 𝑒) = {𝑟 ∈ 𝑁𝑅+ | (𝑑, 𝑒) ∈ 𝑟ℐ }.


3. From Circumscription to Pointwise Circumscription
The framework of circumscribed DLs was introduced in [17, 4]. To combine circumscription with
DLs, the authors introduce the notion of circumscription patterns, declaring how predicates are
handled during the minimization process. A circumscription pattern is a triple 𝒫 = (𝑀, 𝑉, 𝐹 )
declaring three mutually disjoint sets of minimized predicates 𝑀 , varying predicates 𝑉 , and
fixed predicates 𝐹 . A circumscription pattern 𝒫 induces a preference relation ≤𝒫 between
interpretations. Given two interpretations ℐ and 𝒥 , we write ℐ ≤𝒫 𝒥 if the following hold:
(i) Δℐ = Δ𝒥 and 𝑜ℐ = 𝑜𝒥 , for all 𝑜 ∈ 𝑁𝐼 , (ii) for all 𝑝 ∈ 𝑀 , 𝑝ℐ ⊆ 𝑝𝒥 , (iii) for all 𝑝 ∈ 𝐹 ,
𝑝ℐ = 𝑝𝒥 . We write ℐ <𝒫 𝒥 , if ℐ ≤𝒫 𝒥 and 𝑝ℐ ⊂ 𝑝𝒥 for some 𝑝 ∈ 𝑀 . A circumscribed
knowledge base Circ𝒫 (𝒦) is a knowledge base 𝒦 equipped with a circumscription pattern 𝒫.
A model of Circ𝒫 (𝒦) is a model of 𝒦 that is minimal w.r.t. <𝒫 . In [4], the authors provided
a characterization of the complexity of reasoning in different fragments of 𝒜ℒ𝒞ℐ𝒪𝒬. In
particular, allowing roles to be minimized, reasoning turns out to be undecidable even in
circumscribed 𝒜ℒ𝒞.
   We now introduce pointwise circumscription for DLs. To capture some of the possible variants
of (local) minimization, we use a family of comparability relations between interpretations. Note
that any interpretation ℐ can be seen as a directed labeled graph, where each node is labeled
with a collection of concept names and individuals, while each edge is labeled with a collection
of role names. We start with the basic comparability relation.
Definition 1. For a pair of interpretations ℐ, 𝒥 we write ℐ ∼B 𝒥 if Δℐ = Δ𝒥 and 𝑎ℐ = 𝑎𝒥 for
all individuals 𝑎.
   The definition above encodes condition (i) of the preference relation <𝒫 . Two interpretations
ℐ and 𝒥 are 𝐵-comparable if they have the same domain and interpret all individuals in the
same way. We define the binary relation ∼CL (resp. ∼CLs ) that relates two interpretations that
differ by at most one concept label (resp. a set of concept labels) decorating at most one node.
Definition 2. Assume two interpretations ℐ, 𝒥 with ℐ ∼B 𝒥 . We write ℐ ∼CL 𝒥 , if there exists
an object 𝑒 and a concept name 𝐴 such that (i) 𝑟ℐ = 𝑟𝒥 for all role names 𝑟, (ii) 𝐵 ℐ = 𝐵 𝒥 for
all concept names 𝐵 ̸= 𝐴, and (iii) 𝐴ℐ ∖ {𝑒} = 𝐴𝒥 ∖ {𝑒}. We write ℐ ∼CLs 𝒥 if there exists an
object 𝑒 such that (i) 𝑟ℐ = 𝑟𝒥 for all role names 𝑟, and (ii) 𝐴ℐ ∖ {𝑒} = 𝐴𝒥 ∖ {𝑒} for all concept
names 𝐴.
  We introduce the binary relation ∼RL (resp. ∼RLs ) that relates two interpretation in terms of
a modification of a single role label (resp. a collection of role labels) at one edge.
Definition 3. Assume two interpretations ℐ, 𝒥 with ℐ ∼B 𝒥 . We write ℐ ∼RL 𝒥 if there exist
objects 𝑒, 𝑒′ and a role name 𝑟 such that (i) 𝐴ℐ = 𝐴𝒥 for all concept names 𝐴, (ii) 𝑝ℐ = 𝑝𝒥
for all role names 𝑝 ̸= 𝑟, and (iii) 𝑟ℐ ∖ {(𝑒, 𝑒′ )} = 𝑟𝒥 ∖ {(𝑒, 𝑒′ )}. We write ℐ ∼RLs 𝒥 if there
exist objects 𝑒, 𝑒′ such that (i) 𝐴ℐ = 𝐴𝒥 for all concept names 𝐴, (ii) 𝑟ℐ ∖ {(𝑒, 𝑒′ ), (𝑒′ , 𝑒)} =
𝑟𝒥 ∖ {(𝑒, 𝑒′ ), (𝑒′ , 𝑒)} for all role names 𝑟.
   We introduce a star comparability relation, where ℐ and 𝒥 are comparable if there is at most
one node 𝑒 on which ℐ and 𝒥 disagree, i.e. for one node 𝑒, they might disagree on the concept
labeling 𝑒 or the roles labeling some edges involving 𝑒.
Definition 4. Assume two interpretations ℐ, 𝒥 with ℐ ∼B 𝒥 . We write ℐ ∼ST 𝒥 if there exists
an object 𝑒 such that: (i) 𝐴ℐ ∖ {𝑒} = 𝐴𝒥 ∖ {𝑒} for all concept names 𝐴, and (ii) 𝑟ℐ ∩ (Δ × Δ) =
𝑟𝒥 ∩ (Δ × Δ) for all role names 𝑟, where Δ = Δℐ ∖ {𝑒}.
Proposition 1. Given two interpretations ℐ and ℐ ′ : (i) if ℐ ∼CL ℐ ′ then ℐ ∼CLs ℐ ′ ; (ii) if
ℐ ∼RL ℐ ′ then ℐ ∼RLs ℐ ′ ; (iii) if ℐ ∼CLs ℐ ′ or ℐ ∼RLs ℐ ′ then ℐ ∼ST ℐ ′ .
   We can now define various versions of pointwise circumscription, parametrized by a concrete
comparability relation ∼∘ . Circumscription patterns are defined as for classical circumscription.
In the following sections, while comparing two interpretations ℐ and 𝒥 via a comparability
relation ∼∘ to explicitly state the node 𝑒 (resp. the pair of nodes (𝑒, 𝑒′ )) at which they may
differ in terms of labels, we write ∼∘𝑒 (resp. ∼∘(𝑒,𝑒′ ) ).

Definition 5. Assume a circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ), a pair of interpretations ℐ, 𝒥 ,
and let ∘ ∈ {B, CL, CLs, RL, RLs, ST}. We write ℐ ⪯∘𝒫 𝒥 if the following conditions hold:
 (i) 𝑄ℐ ⊆ 𝑄𝒥 for all 𝑄 ∈ 𝑀 ,
 (ii) 𝑄ℐ = 𝑄𝒥 for all 𝑄 ∈ 𝐹 , and
(iii) ℐ ∼∘ 𝒥 .

We write: (a) ℐ ≺∘𝒫 𝒥 , if ℐ ⪯∘𝒫 𝒥 and 𝑄ℐ ⊂ 𝑄𝒥 for some 𝑄 ∈ 𝑀 , and (b) ℐ ⪯∘𝒫,𝑒 𝒥 if ℐ ∼∘𝑒 𝒥 .
We denote with Circ∘𝒫 (𝒦) a pointwise circumscribed KB 𝒦, i.e., a knowledge base equipped with
a circumscription pattern 𝒫, where ∘ ∈ {B, CL, CLs, RL, RLs, ST}. An interpretation ℐ is a
model of Circ∘𝒫 (𝒦), if ℐ |= 𝒦 and there is no intepretation 𝒥 s.t. 𝒥 |= 𝒦 and 𝒥 ≺∘𝒫 ℐ.
  We focus on the reasoning tasks of concept satisfiability, concept subsumption and instance
checking w.r.t. pointwise circumscribed KBs. As shown for circumscribed DLs in [4], the afore-
mentioned reasoning tasks can be polynomially reduced one into the other.
Definition 6. Assume a KB 𝒦 and a circumscription pattern 𝒫. Given two concepts 𝐶0 and 𝐷0
in 𝒜ℒ𝒞ℐ𝒪 and 𝑎 ∈ 𝑁𝐼 :
    • 𝐶0 is satisfiable w.r.t. Circ∘𝒫 (𝒦) if there exists a model ℐ of Circ∘𝒫 (𝒦) such that 𝐶0ℐ ̸= ∅;
    • 𝐶0 is subsumed by 𝐷0 w.r.t. Circ∘𝒫 (𝒦), and we write Circ∘𝒫 (𝒦) |= 𝐶0 ⊑ 𝐷0 , if 𝐶0ℐ ⊆ 𝐷0ℐ
      in any model ℐ of Circ∘𝒫 (𝒦);
    • 𝑎 is an instance of a concept 𝐶0 w.r.t Circ∘𝒫 (𝒦), and we write Circ∘𝒫 (𝒦) |= 𝐶0 (𝑎), if 𝑎ℐ ∈ 𝐶0ℐ
      in all models ℐ of Circ∘𝒫 (𝒦).
Example 1. We reformulate the example in [18] on the situs inversus, a condition affecting those
humans whose heart is located on the right-hand side of the body. Consider TBox 𝒯SI defined as
follows

Situs_Inversus ⊑ Human                                      Situs_Inversus⊑ ∃has_heart.Right
Human ⊓ ¬Situs_Inversus⊑ ∃has_heart.Left                    Left ⊓ Right ⊑ ⊥


with the circumscription pattern 𝒫 with 𝑀 ={Situs_Inversus, has_heart} and
𝐹 = {Human, Right, Left}. Since the role has_heart is minimized, no heart can be po-
sitioned on both sides of the body. As in classic circumscription, with the ST semantics, we derive
that
                   CircST
                       𝒫 (𝒯SI ) |= Human ⊑ ∃has_heart.Left        and
                   CircST
                       𝒫 (𝒯SI ) |= Human ⊓ ∃has_heart.Right ⊑ Situs_Inversus

 i.e. normally humans have the heart positioned on the left-hand side of the body and humans
affected by the situs inversus are all and only the humans whose heart is positioned on the right-hand
side of the body.
  Of these variants of pointwise circumscription, the one induced by ∼ST is the strongest.
Proposition 2. Assume a knowledge base 𝒦 and a circumscription pattern 𝒫. If ℐ is a model of
CircST                             RLs           CLs
    𝒫 (𝒦) then ℐ is a model of Circ𝒫 (𝒦) and Circ𝒫 (𝒦).

  In what follows, we focus on pointwise circumscription induced by ∼ST , and given a circum-
scription pattern 𝒫, by minimality we mean minimality with respect to ≺ST𝒫 .


4. A Method for Reasoning under Pointwise Circumscription
We now provide a method for reasoning under pointwise circumscription in TBoxes in a fragment
of the very expressive DL 𝒜ℒ𝒞ℐ𝒪 with no restrictions on the circumscription patterns, and
show that in this setting, the computational complexity of reasoning is in (co)NExpTime.
   We consider a pointwise circumscribed fragment of 𝒜ℒ𝒞ℐ𝒪 that we call 1-𝒜ℒ𝒞ℐ𝒪, where
we only allow for some concepts of depth at most one. We denote with 𝑑(𝐶) the (modal) depth
of an 𝒜ℒ𝒞ℐ𝒪 concept 𝐶 (defined as the maximum number of nested quantifiers). In 1-𝒜ℒ𝒞ℐ𝒪
only the following axiom shapes are allowed:
                          𝐷1 ⊑ 𝐷2         𝐷1 ⊑ ∃𝑟.𝐷2         𝐷1 ⊑ ∀𝑟.𝐷2
with 𝑑(𝐷1 ) = 𝑑(𝐷2 ) = 0. For simplicity, we consider 1-𝒜ℒ𝒞ℐ𝒪 TBoxes in normal form,
containing only axioms of the shapes:
                             𝐷1 ⊑ 𝐷2         𝐴 ⊑ ∃𝑟.𝐵        𝐴 ⊑ ∀𝑟.𝐵
with 𝐴, 𝐵 ∈ 𝑁𝐶+ . That is, existential and universal axioms involve only basic concepts. We can
apply a normalization procedure to TBoxes in 1-𝒜ℒ𝒞ℐ𝒪, introducing fresh concept names for
the boolean combinations in quantified axioms, e.g., 𝐷1 ⊑ 𝑄𝑟.𝐷2 , with 𝑄 ∈ {∃, ∀}, can be
replaced by 𝐴1 ⊑ 𝑄𝑟.𝐴2 , 𝐴1 ≡ 𝐷1 , 𝐴2 ≡ 𝐷2 , where 𝐴1 , 𝐴2 are fresh concept names.
Proposition 3. Assume a TBox 𝒯 in 1-𝒜ℒ𝒞ℐ𝒪 and a circumscription pattern 𝒫, let 𝒯 ′ be the
normalization of 𝒯 and let 𝒫 ′ = (𝑀, 𝑉 ∪ 𝑁, 𝐹 ) be the circumscription pattern extended with the
set 𝑁 of fresh concept names introduced by the normalization. A concept name 𝐶0 is satisfiable
w.r.t. 𝐶𝑖𝑟𝑐ST                                                 ST    ′
           𝒫 (𝒯 ) if and only if 𝐶0 is satisfiable w.r.t. 𝐶𝑖𝑟𝑐𝒫 ′ (𝒯 ).
  We note that, in general, this form of normalization does not preserve minimality even if the
TBox is ‘almost’ in normal from. This is shown in the following example.
Example 2. Consider the TBox 𝒯 = {𝐴 ⊑ ∃𝑟.𝐵 ⊔ 𝐶} with the circumscription pattern 𝒫 =
(𝑀, 𝑉, 𝐹 ) with 𝑀 = {𝐵} and 𝐹 = {𝐴, 𝐶, 𝑟}. Consider 𝒯 ′ = {𝐴 ⊑ 𝐸 ⊔ 𝐶, 𝐸 ≡ ∃𝑟.𝐵}
obtaianed renaming the complex concepts in 𝒯 . Let 𝒫 ′ = (𝑀, 𝑉 ∪ {𝐸}, 𝐹 ), the interpretation ℐ
with Δℐ = {𝑒1 , 𝑒2 }, 𝑢𝑡ℐ (𝑒1 ) = {𝐵, 𝐸, 𝐶}, 𝑢𝑡ℐ (𝑒2 ) = {𝐵} and 𝑏𝑡ℐ (𝑒1 , 𝑒2 ) = {𝑟} is a model of
CircST    ′                        ′
    𝒫 ′ (𝒯 ). The interpretation ℐ = ℐ|𝑠𝑖𝑔(𝒯 ) obtained restricting ℐ to the signature of 𝒯 is not a
model of CircST𝒫 (𝒯 ). The same happens if 𝐸 is minimized or fixed.
  In the rest of this section, we assume a fixed 1-𝒜ℒ𝒞ℐ𝒪 TBox 𝒯 in normal form. Note
that we do not consider ABoxes since in 1-𝒜ℒ𝒞ℐ𝒪 they can be incorporated into the TBox,
adding (i) for each 𝐴(𝑎) ∈ 𝒜, the axiom {𝑎} ⊑ 𝐴, and (ii) for each 𝑟(𝑎, 𝑏) ∈ 𝒜, the axiom
{𝑎} ⊑ ∃𝑟.{𝑏}. Our algorithm uses a mosaic technique [13] to show that the existence of a model
can be established by finding a suitable set of small model fragments, which we call star types.
Importantly, minimality can be guaranteed locally at the star types.
  Given a model ℐ of 𝒯 and an element 𝑑 ∈ Δℐ , we extract a structure containing the
description of the unary type of the element and its direct neighbors in the structure, i.e. all
those elements connected via some role 𝑟 to 𝑑.
Definition 7. Let 𝑥 be a symbol, called the center placeholder. Let 𝑁𝑌 be a countably infinite
set of symbols s.t. 𝑥 ̸∈ 𝑁𝑌 , where each 𝑦 ∈ 𝑁𝑌 is called a spike placeholder. A star type 𝜏 is an
interpretation such that:
 (i) Δ𝜏 = 𝑆(𝜏 ) ∪ {𝑥}, where 𝑆(𝜏 ) ⊆ 𝑁𝑌 (called the set of spike placeholders in 𝜏 ),
 (ii) if 𝑦 ∈ Δ𝜏 ∩ 𝑁𝑌 , then (𝑥, 𝑦) ∈ 𝑟𝜏 for some role 𝑟,
(iii) for all roles 𝑟, (𝑐, 𝑑) ∈ 𝑟𝜏 iff either 𝑐 = 𝑥 or 𝑑 = 𝑥.

  We require the local satisfiability of TBox axioms via the notion of suitable star type; note
that satisfaction of the existential axioms is required only at the center.
Definition 8. A type 𝜏 is suitable for 𝒯 if the following conditions are satisfied:
(a) for all 𝐷1 ⊑ 𝐷2 ∈ 𝒯 and for any 𝑑 ∈ Δ𝜏 , if 𝑑 ∈ 𝐷1𝜏 then 𝑑 ∈ 𝐷2𝜏 ,
(b) for all 𝐴 ⊑ ∃𝑟.𝐵 ∈ 𝒯 , if 𝑥 ∈ 𝐴𝜏 , there exists 𝑦 ∈ 𝑆(𝜏 ) such that (𝑥, 𝑦) ∈ 𝑟𝜏 and 𝑦 ∈ 𝐵 𝜏 ,
(c) for all 𝐴 ⊑ ∀𝑟.𝐵 ∈ 𝒯 , if 𝑑 ∈ 𝐴𝜏 , then for any 𝑑′ ∈ Δ𝜏 s.t. (𝑑, 𝑑′ ) ∈ 𝑟𝜏 , 𝑑′ ∈ 𝐵 𝜏 .

  To ensure that star types are locally minimal, we need some additional book-keeping. Consider
the set 𝐸𝑥 = {∃𝑟.𝐶| 𝑟 ∈ 𝑁𝑅+ and 𝐶 ∈ 𝑁𝐶+ }. We now extend the notion of star type with two
additional components ℓ𝑐 and ℓ𝑖 , labeling the spikes with elements in 𝐸𝑥.
Definition 9. An adorned star type is a structure (𝜏, ℓ𝑐 , ℓ𝑖 ) such that 𝜏 is a suitable star type for
𝒯 and ℓ𝑐 , ℓ𝑖 : 𝑆(𝜏 ) → 2𝐸𝑥 are defined as follows:
 (i) ∃𝑟.𝐶 ∈ ℓ𝑐 (𝑦) if and only if
     (a) there exists 𝐴 ⊑ ∃𝑟.𝐶 ∈ 𝒯 such that 𝑥 ∈ 𝐴𝜏 , (𝑥, 𝑦) ∈ 𝑟𝜏 , and 𝑦 ∈ 𝐵 𝜏 , and
     (b) there exists no 𝑦 ′ ∈ Δ𝜏 s.t. 𝑦 ′ ̸= 𝑦 and (1) (𝑥, 𝑦 ′ ) ∈ 𝑟𝜏 , and (2) 𝑦 ′ ∈ 𝐵 𝜏 ;
 (ii) ∃𝑟.𝐵 ∈ ℓ𝑖 (𝑦) only if there exists 𝐴 ⊑ ∃𝑟.𝐵 ∈ 𝒯 such that 𝑦 ∈ 𝐴𝜏 , (𝑦, 𝑥) ∈ 𝑟𝜏 , and 𝑥 ∈ 𝐵 𝜏 .

Definition 10. Assume a circumscription pattern 𝒫. A suitable adorned star type (𝜏, ℓ𝑐 , ℓ𝑖 ) for 𝒯
is minimal if there is no interpretation 𝒥 such that (1) 𝒥 ≺ST
                                                            𝒫,𝑥 𝜏 , (2) 𝒥 satisfies conditions (𝑎)-(𝑐)
in Definition 8, and (3) for each 𝑦 ∈ 𝑆(𝜏 ) such that ∃𝑟.𝐶 ∈ ℓ𝑖 (𝑦) then (𝑦, 𝑥) ∈ 𝑟𝒥 and 𝑥 ∈ 𝐶 𝒥 .
  We define abstract types as compact descriptions of star types. While the latter may have an
arbitrary number of spikes, the former store only a bounded, relevant neighborhood. First, we
define the set of all possible unary types for 𝒯 .
Definition 11. 𝑇 ⊆ 𝑁𝐶+ is a type for 𝒯 if ⊤ ∈ 𝑇 and ⊥ ̸∈ 𝒯 and for all 𝑎, 𝑏 ∈ 𝑁𝐼 (𝒯 ), if
{𝑎}, {𝑏} ∈ 𝑇 , then 𝑎 = 𝑏. We denote with Types(𝒯 ) the set of types for 𝒯 .
   Now we define abstract types. Our approach is similar to the one in [15, 14], but we add
more information to the description of the neighbors of an element, matching the meaning
of the labeling functions ℓ𝑐 and ℓ𝑖 in the star types. To this end, we define the set L =
{(∃𝑟.𝐵, 𝑙)| with 𝑙 ∈ {𝑢, 𝑓, 𝑠}, 𝑟 ∈ 𝑁𝑅+ and 𝐵 ∈ 𝑁𝐶+ } where the letters 𝑢, 𝑓, 𝑠 stand for
unique, first and second, the meaning whereof we clarify below the following definition. Given
a concept 𝐶 such that 𝑑(𝐶) = 0 and 𝑇 ∈ Types(𝒯 ), for some TBox 𝒯 , we write 𝑇 |=0 𝐶 if
intuitively seeing 𝐶 as a formula and 𝑇 as an interpretation, 𝐶 is satisfied in 𝑇 .
Definition 12. Let 𝒯 be a normalized TBox in 𝒜ℒ𝒞ℐ𝒪. An abstract type is a pair (𝑇, 𝜌)
such that 𝑇 ∈ Types(𝒯 ) and 𝜌 is a set of tuples (𝑅, 𝑇 ′ , 𝐿𝑐 , 𝐿𝑖 ), we call abstract spikes, with
∅ ⊂ 𝑅 ⊆ 𝑁𝑅+ (𝒯 ), 𝑇 ′ ⊆ 𝑁𝐶+ (𝒯 ) and 𝐿𝑐 , 𝐿𝑖 ⊆ L, satisfying the following conditions:
1) |𝜌| ≤ 4 ‖𝒯 ‖;
2) if 𝐷1 ⊑ 𝐷2 ∈ 𝒯 and 𝑇 |=0 𝐷1 , then 𝑇 |=0 𝐷2 ;
3) for all 𝐴 ⊑ ∃𝑟.𝐵 ∈ 𝒯 s.t. 𝐴 ∈ 𝑇 , there is (𝑅, 𝑇 ′ , 𝐿𝑐 , 𝐿𝑖 ) ∈ 𝜌 s.t. 𝑟 ∈ 𝑅 and 𝐵 ∈ 𝑇 ′ ;
4) for all (𝑅, 𝑇 ′ , 𝐿𝑐 , 𝐿𝑖 ) ∈ 𝜌 the following hold:
     (i) if 𝐴 ⊑ ∀𝑟.𝐵 ∈ 𝒯 , 𝐴 ∈ 𝑇 and 𝑟 ∈ 𝑅, then 𝐵 ∈ 𝑇 ′ ,
    (ii) if 𝐴 ⊑ ∀𝑟.𝐵 ∈ 𝒯 , 𝐴 ∈ 𝑇 ′ and 𝑟− ∈ 𝑅, then 𝐵 ∈ 𝑇 ;
5) (∃𝑟.𝐵, 𝑙) ∈ 𝐿𝑐 only if there exists 𝐴 ⊑ ∃𝑟.𝐵 ∈ 𝒯 such that 𝐴 ∈ 𝑇 , 𝑟 ∈ 𝑅 and 𝐵 ∈ 𝑇 ′ ;
6) (∃𝑟.𝐵, 𝑙) ∈ 𝐿𝑖 only if there exists 𝐴 ⊑ ∃𝑟.𝐵 ∈ 𝒯 such that 𝐴 ∈ 𝑇 ′ , 𝑟− ∈ 𝑅 and 𝐵 ∈ 𝑇 .

Given the set 𝐸𝑥(𝑇, 𝜌) = {(𝑟, 𝐵)| there exists 𝐴 ⊑ ∃𝑟.𝐵 ∈ 𝒯 and 𝐴 ∈ 𝑇 }, we define a function
𝑤𝑖𝑡(𝑇,𝜌) : 𝐸𝑥(𝑇, 𝜌) → 2𝜌 such that 𝑤𝑖𝑡(𝑇,𝜌) ((𝑟, 𝐵)) = {(𝑅, 𝑇 ′ , 𝐿𝑐 , 𝐿𝑖 ) ∈ 𝜌| 𝑟 ∈ 𝑅 ∧ 𝐵 ∈ 𝑇 ′ }
and we require that the two sets 𝐿𝑐 and 𝐿𝑖 satisfy the following conditions:
  (i) for all (𝑟, 𝐵) ∈ 𝐸𝑥(𝑇, 𝜌), (∃𝑟.𝐵, 𝑢) ∈ 𝐿𝑐 only if 𝑤𝑖𝑡(𝑇,𝜌) ((𝑟, 𝐵)) = {(𝑅, 𝑇 ′ , 𝐿𝑐 , 𝐿𝑖 )};
 (ii) for all (𝑟, 𝐵) ∈ 𝐸𝑥(𝑇, 𝜌) such that |𝑤𝑖𝑡(𝑇,𝜌) ((𝑟, 𝐵))| > 1, there exists exactly one spike 𝑦1
      such that (∃𝑟.𝐵, 𝑓 ) ∈ 𝐿𝑐 and exactly one spike 𝑦2 such that (∃𝑟.𝐵, 𝑠) ∈ 𝐿𝑐 .

   The bound on the number of spikes ensures that the number of abstract types is exponential
in the size of the TBox. Conditions (i) and (ii) ensure the correct meaning of the labeling sets
𝐿𝑐 and 𝐿𝑖 and ensure the consistency between the intended information of the letter 𝑙 and
the actual content of 𝜌: whenever a spike has a label (∃𝑟.𝐵, 𝑠) (resp. 𝑓 ), for some basic role 𝑟
and some basic concept 𝐵, we explicitly require that there exists another spike with the label
(∃𝑟.𝐵, 𝑓 ) (resp. 𝑠). In a nutshell, any second ‘witness’ must have a first ‘witness’, and vice versa.
   There is a clear parallelism between abstract types and star types. We rely on star types as
concrete realizations of abstract types, associating to each abstract type (𝑇, 𝜌) a specific star
type instantiating all and only the information enclosed in it.
Definition 13. Given an abstract type (𝑇, 𝜌), we call canonic instance of (𝑇, 𝜌) the adorned star
type (𝜏(𝑇,𝜌) , ℓ𝑐 , ℓ𝑖 ) such that 𝑢𝑡(𝑥) = 𝑇 and
  (i) for each abstract spike 𝑠 = (𝑅, 𝑇 ′ , 𝐿𝑐 , 𝐿𝑖 ) ∈ 𝜌, there exists a unique spike 𝑦𝑠 such
      that (1) ℓ𝑐 (𝑦𝑠 ) = {∃𝑟.𝐵| (∃𝑟.𝐵, 𝑢) ∈ 𝐿𝑐 } and ℓ𝑖 (𝑦𝑠 ) = {∃𝑟.𝐵| (∃𝑟.𝐵, 𝑢) ∈ 𝐿𝑖 },
      (2) 𝑏𝑡(𝑥, 𝑦𝑠 ) = 𝑅 and (3) 𝑢𝑡(𝑦𝑠 ) = 𝑇 ′ ,
 (ii) there are no further spikes, that is |𝑆(𝜏(𝑇,𝜌) )| = |𝜌|.

Definition 14. Assume a TBox 𝒯 and a concept 𝐶0 in 𝒜ℒ𝒞ℐ𝒪 such that 𝑑(𝐶0 ) ≤ 1. For any
                                                                𝜏
abstract type (𝑇, 𝜌), we write (𝑇, 𝜌) |= 𝐶0 if and only if 𝑥 ∈ 𝐶0(𝑇,𝜌) .
Definition 15. Given a circumscription pattern 𝒫 and an 𝒜ℒ𝒞ℐ𝒪 TBox 𝒯 , an abstract star type
is minimal if and only if its canonical instance is minimal.
   We denote ST(𝒯 , 𝒫) the set of all minimal abstract types for a TBox 𝒯 w.r.t a circumscription
pattern 𝒫. Intuitively, we want to describe minimal models by putting together minimal abstract
start types. Before characterizing when a set of minimal star types represents a minimal model,
we need a compatibility condition that ensures that minimality of a type is preserved when
attaching it to another one via a spike.
Definition 16. Assume an 𝒜ℒ𝒞ℐ𝒪 TBox 𝒯 and a circumscription pattern 𝒫 = (𝑀, 𝐹, 𝑉 ). Let
(𝑇, 𝜌) ∈ ST(𝒯 , 𝒫) and 𝑠 = (𝑅, 𝑇 ′ , 𝐿𝑐 , ∅) ∈ 𝜌. Given (𝑇 ′ , 𝜌′ ) ∈ ST(𝒯 , 𝒫), 𝜌′ is compatible with
𝑠 if and only if for all 𝑟 ∈ 𝑅− and 𝐵 ∈ 𝑇 and for all (𝑅′ , 𝑇 ′′ , 𝐿′𝑐 , 𝐿′𝑖 ) ∈ 𝜌′ , (∃𝑟.𝐵, 𝑢) ̸∈ 𝐿′𝑐 .
  Let N* = N ∪ {∞} such that for all 𝑛 ∈ N, 𝑛 + ∞ = ∞, 𝑛 · ∞ = ∞, ∞ + ∞ = ∞ and
∞ · ∞ = ∞. Following [14, 15], the system of inequalities in Theorem 1 is called enriched
system of inequalities. Inequalities of the shapes (3)-(4) form a so-called positive enriched system.
Theorem 1. Assume a TBox 𝒯 in normal form and a concept a 𝐶0 with 𝑑(𝐶0 ) ≤ 1. Given
circumscription pattern 𝒫 = (𝑀, 𝑉, 𝐹 ), 𝐶0 is satisfiable w.r.t. CircST
                                                                     𝒫 (𝒯 ) if and only if there
                                    *
exists a function 𝑁 : 𝑆𝑇 (𝒯 , 𝒫) → N such that the following conditions are satisfied:
(1) For all 𝑎 ∈ 𝑠𝑖𝑔(𝒯 ), the following inequality holds:
                                          ∑︁
                                                      𝑁 ((𝑇, 𝜌)) = 1
                                     (𝑇,𝜌)∈𝑆𝑇 (𝒯 ,𝒫)∧{𝑎}∈𝑇

                                                        ∑︁
(2) The following inequality holds:                                         𝑁 ((𝑇, 𝜌)) ≥ 1
                                           (𝑇,𝜌)∈𝑆𝑇 (𝒯 ,𝒫)∧(𝑇,𝜌)|=𝐶0

(3) For any pair of types 𝑇, 𝑇 ′ ⊆ 𝑁𝐶+ (𝒯 ) and for any set of roles 𝑅 ⊆ 𝑁𝑅+ and any 𝐿𝑐 , 𝐿𝑖 ⊆ L:
                                   ∑︁                                       ∑︁
                                                     𝑁 (𝑇, 𝜌) ≤                            𝑁 (𝑇 ′ , 𝜌′ )
                            (𝑇,𝜌)∈ST(𝒯 ,𝒫)                          ′   ′
                                                                  (𝑇 ,𝜌 )∈ST(𝒯 ,𝒫)∧
                         (𝑅,𝑇 ′ ,𝐿𝑐 ,𝐿𝑖 )∈𝜌∧𝐿𝑖 ̸=∅                 (𝑅− ,𝑇,𝐿𝑖 ,𝐿𝑐 )∈𝜌


(4) For any pair of types 𝑇, 𝑇 ′ ⊆ 𝑁𝐶+ (𝒯 ) and for any set of roles 𝑅 ⊆ 𝑁𝑅+ and any 𝐿𝑐 ⊆ L:
                          ∑︁                                                 ∑︁
                                         𝑁 (𝑇, 𝜌) > 0 implies                              𝑁 (𝑇 ′ , 𝜌′ ) > 0
                     (𝑇,𝜌)∈ST(𝒯 ,𝒫)                                (𝑇 ′ ,𝜌′ )∈ST(𝒯 ,𝒫)
                    𝑠=(𝑅,𝑇 ′ ,𝐿𝑐 ,∅)∈𝜌                             ∧𝜌′ compatible with 𝑠
                                 𝐺𝑁                                                      𝐺𝑁
                         𝑜 (0, 0)                                                𝑜 (0, 0)
                     𝑣       ℎ                                               𝑣       ℎ
         (0, 1)𝐺𝑁                  (1, 0)𝐺𝑁                      (0, 1)𝐺𝑁                  (1, 0)𝐺𝑁

                ℎ                  𝑣                                    ℎ    ℎ             𝑣

            (1, 1)               𝑑 (1, 1)                           (1, 1)               𝑑 (1, 1)𝐺𝑁,𝐶

(a) Initial situation: the minimization of ℎ and        (b) Requiring the satisfiability of 𝐶 enforces the
    𝑣 alone does not enforce a grid.                        existence of a unique good node (1, 1).
Figure 1: Enforcement of a 2 × 2 grid with pointwise circumscription. We bypass functionality, ensuring
the existence of a unique horizontal (ℎ-)predecessor and vertical (𝑣-)predecessor via minimization.


  The function 𝑁 associates to each abstract type the number of instances needed for building
a model. Conditions (1)-(2) ensure the correct encoding of nominals and the satisfiability of 𝐶0 .
Conditions (3)-(4) guarantee that for each realized abstract type there exist a ‘successor’ for
each spike. Intuitively in (3), for each spike with 𝐿𝑖 ̸= ∅ in a realized abstract type, we require
the realization of an abstract type overlapping at that spike. The inequality (3) ensures the
existence of enough overlapping abstract types. Condition (4) specifically deals with preserving
minimality while constructing the model.
Theorem 2 ([14]). Deciding the existence of a solution for an enriched system of inequalities
𝐻 is feasible in non-deterministic polynomial time in the size of 𝐻. If 𝐻 contains only positive
inequalities, the problem is solvable in polynomial time in the size of 𝐻.
  The corollary below directly follows from Theorem 1 and Theorem 2.
Corollary 1. In 𝒜ℒ𝒞ℐ𝒪, satisfiability of concepts of depth at most 1 w.r.t. pointwise circumscribed
KBs in normal form is in NExpTime.
  The following corollary is a consequence of Proposition 3 and Corollary 1.
Corollary 2. In pointwise circumscribed 1-𝒜ℒ𝒞ℐ𝒪, satisfiability of concepts of depth at most
one is in NExpTime.
  Recalling that concept satisfiability, subsumption and instance checking can be polynomially
reduced one into the other, the following corollary holds.
Corollary 3. In 1-𝒜ℒ𝒞ℐ𝒪, for concepts of depth at most one, subsumption and instance checking
w.r.t. pointwise circumscribed TBoxes are in coNExpTime.
  Observe that the TBox 𝒯SI of Example 1 is in 1-𝒜ℒ𝒞ℐ𝒪. In contrast with classically circum-
scribed DLs, 𝒯SI falls in decidable fragment of pointwise circumscribed DLs.


5. Lower Bound
We provide a reduction from the exponential grid tiling problem to concept satisfiability w.r.t.
pointwise circumscribed TBoxes in 𝒜ℒ𝒞ℐ𝒪. Differently from the reduction proposed for
𝒜ℒ𝒞ℐ𝒪ℱ [16], we bypass functionality using minimality.
Theorem 3. In 1-𝒜ℒ𝒞ℐ𝒪, concept name satisfiability w.r.t. pointwise circumscribed TBoxes is
NExp-hard.

   We briefly discuss the key ideas here. Given an instance of the exponential grid tiling problem
𝑃 , we build a TBox 𝒯𝑃 and a circumscription pattern 𝒫 such that, in any model ℐ of Circ𝒫 (𝒯𝑃 ),
each domain element 𝑑 is uniquely associated to a position (𝑥𝑑 , 𝑦𝑑 ) in the 2𝑛 × 2𝑛 grid. The
origin (0, 0) corresponds to a nominal 𝑜. With special care for boundary nodes of the grid, each
element has exactly one ℎ-successor (horizontal) and one 𝑣-successor (vertical). To enforce
uniqueness, we require that ℎ and 𝑣 are minimized. Via counting axioms (see [16]), we encode a
correct updating of the coordinates 𝑥 and 𝑦.
   We call good node any node intuitively corresponding to a correct node in the grid, i.e. with
a unique incoming ℎ and a unique incoming 𝑣. We denote good nodes with the minimized
concept 𝐺𝑁 . The notion of good node is adapted to deal with nodes of coordinates (0, 𝑦) and
(𝑥, 0). For 𝑛 = 1, we obtain the structure in Figure 1a, where (𝑥, 𝑦)𝐺𝑁 denotes that the node
of coordinates (𝑥, 𝑦) is a good node. We check the satisfiability of a minimized concept 𝐶.
Introducing appropriate axioms, given a minimal model ℐ, we require that 𝑑 ∈ 𝐶 ℐ if and only if
(𝑥𝑑 , 𝑦𝑑 ) = (2𝑛 − 1, 2𝑛 − 1) and 𝑑 ∈ 𝐺𝑁 ℐ . Since 𝐺𝑁 is minimized and 𝑥𝑑 , 𝑦𝑑 ̸= 0, we ensure
that there must exist an ℎ-predecessor and a 𝑣-predecessor for 𝑑 that are good nodes too. Figure
1b represents a model of Circ𝒫 (𝒯𝑃 ) where 𝐶 is satisfiable. The minimization of 𝐺𝑁 and the
roles ℎ, 𝑣 with the condition on the nominal 𝑜 imply that there cannot be any other extra good
node as ℎ-predecessor for 𝑑, enforcing the grid.


6. Discussion
In this paper, we have presented our preliminary work on pointwise circumscription in DLs, as
an alternative to classic circumscription: we aimed at lowering the computational complexity,
while still maintaining sufficient expressiveness.
   Many directions remain open for future work. The results presented here are for TBoxes of
restricted shape, and hence the first direction is to study a larger class of TBoxes. We believe
that our technique and the upper bounds also apply to TBoxes in a relaxed normal form, where
arbitrary inclusions between concepts with modal depth 1 are allowed. An interesting next step
is to consider satisfiability and subsumption of general concepts (with unbounded modal depth)
under TBoxes in both of these normal forms. Naturally, we plan to investigate the complexity
of reasoning with general TBoxes (with unbounded modal depth), which seems to require
significant new insights. Another interesting direction is to extend our formalism with priorities,
which are important for knowledge representation and are supported in classic circumscription.
   Pointwise circumscription in lightweight DLs and DLs beyond 𝒜ℒ𝒞ℐ𝒪 also remains to be
explored. In [11], classic circumscription is used to provide the semantics to defeasible inclusions
in DLs. We plan to explore whether pointwise circumscription can be applied in this context
as well. Another direction is to study the data complexity of entailment of assertions from
pointwise circumscribed KBs.
Acknowledgments
This work was partially supported by the Vienna Business Agency and the Austrian Science
Fund (FWF) projects P30360 and P30873.


References
 [1] L. Giordano, V. Gliozzi, N. Olivetti, G. L. Pozzato, Reasoning about typicality in preferential
     description logics, in: S. Hölldobler, C. Lutz, H. Wansing (Eds.), Logics in Artificial
     Intelligence, Springer Berlin Heidelberg, Berlin, Heidelberg, 2008, pp. 192–205.
 [2] F. Baader, B. Hollunder, Priorities on defaults with prerequisites, and their application in
     treating specificity in terminological default logic., Journal of Automated Reasoning 15
     (1995) 41–68.
 [3] F. Donini, M. Lenzerini, D. Nardi, W. Nutt, A. Schaerf,                An epistemic opera-
     tor for description logics, Artificial Intelligence 100 (1998) 225–274. URL: https://
     www.sciencedirect.com/science/article/pii/S0004370298000095. doi:https://doi.org/
     10.1016/S0004-3702(98)00009-5.
 [4] P. A. Bonatti, C. Lutz, F. Wolter, The complexity of circumscription in description logic,
     Journal of Artificial Intelligence Research (2009) 717–773.
 [5] P. A. Bonatti, Query answering in circumscribed OWL2 profiles, Ann. Math. Artif. In-
     tell. 89 (2021) 1155–1173. URL: https://doi.org/10.1007/s10472-021-09770-2. doi:10.1007/
     s10472-021-09770-2.
 [6] P. A. Bonatti, M. Faella, C. Lutz, L. Sauro, F. Wolter, Decidability of circumscribed de-
     scription logics revisited, in: T. Eiter, H. Strass, M. Truszczynski, S. Woltran (Eds.),
     Advances in Knowledge Representation, Logic Programming, and Abstract Argumen-
     tation - Essays Dedicated to Gerhard Brewka on the Occasion of His 60th Birthday,
     volume 9060 of Lecture Notes in Computer Science, Springer, 2015, pp. 112–124. URL:
     https://doi.org/10.1007/978-3-319-14726-0_8. doi:10.1007/978-3-319-14726-0\_8.
 [7] P. A. Bonatti, M. Faella, L. Sauro, Defeasible inclusions in low-complexity dls, J. Artif. Intell.
     Res. 42 (2011) 719–764. URL: https://doi.org/10.1613/jair.3360. doi:10.1613/jair.3360.
 [8] J. McCarthy, Circumscription—a form of non-monotonic reasoning, Artificial Intelligence
     13 (1980) 27–39. URL: https://www.sciencedirect.com/science/article/pii/0004370280900119.
     doi:https://doi.org/10.1016/0004-3702(80)90011-9, special Issue on Non-
     Monotonic Logic.
 [9] J. McCarthy, Applications of circumscription to formalizing common-sense knowledge, Ar-
     tificial Intelligence 28 (1986) 89–116. URL: https://www.sciencedirect.com/science/article/
     pii/0004370286900329. doi:https://doi.org/10.1016/0004-3702(86)90032-9.
[10] V. Lifschitz, Closed-world databases and circumscription, Artificial Intelligence 27
     (1985) 229–235. URL: https://www.sciencedirect.com/science/article/pii/0004370285900554.
     doi:https://doi.org/10.1016/0004-3702(85)90055-4.
[11] P. A. Bonatti, M. Faella, L. Sauro, Defeasible inclusions in low-complexity dls, J. Artif. Int.
     Res. 42 (2011) 719–764.
[12] V. Lifschitz, Pointwise circumscription: Preliminary report, in: AAAI, 1986.
[13] I. Németi, Decidable versions of first order logic and cylindric-relativized set algebras, in:
     C. Publications (Ed.), Logic Colloquium ‘92, 1992, pp. 171–241.
[14] T. Gogacz, V. Gutiérrez-Basulto, Y. Ibáñez-García, F. Murlak, M. Ortiz, M. Simkus, Ontology
     focusing: Knowledge-enriched databases on demand, in: ECAI, volume 325 of Frontiers in
     Artificial Intelligence and Applications, IOS Press, 2020, pp. 745–752.
[15] T. Gogacz, S. Lukumbuzya, M. Ortiz, M. Simkus, Datalog rewritability and data complexity
     of ALCHOIF with closed predicates, in: KR, 2020, pp. 434–444.
[16] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
     University Press, Cambridge, UK, 2017.
[17] P. Bonatti, C.Lutz, F. Wolter, Description logics with circumscription, in: Proceedings
     of the Tenth International Conference on Principles of Knowledge Representation and
     Reasoning, KR’06, AAAI Press, 2006, pp. 400–410.
[18] P. Bonatti, I. Petrova, L. Sauro, Defeasible Reasoning in Description Logics: An Overview
     on DLN, volume Volume 49: Applications and Practices in Ontology Design, Extraction,
     and Reasoning. of Studies on the Semantic Web., IOS Press, 2020, pp. 178 – 193.

</pre>