# description_logics_with_pointwise_circumscription__e83fd9eb.pdf

Description Logics with Pointwise Circumscription

Federica Di Stefano1 , Magdalena Ortiz2 and Mantas ˇSimkus2

1Institute of Logic and Computation, TU Wien, Austria 2Department of Computing Science, Ume a University, Sweden federica.stefano@tuwien.ac.at, {magortiz, simkus}@cs.umu.se

Circumscription is one of the most powerful ways to extend Description Logics (DLs) with nonmonotonic reasoning features, albeit with huge computational costs and undecidability in many cases. In this paper, we introduce pointwise circumscription for DLs, which is not only intuitive in terms of knowledge representation, but also provides a sound approximation of classic circumscription and has reduced computational complexity. Our main idea is to replace the secondorder quantiﬁcation step of classic circumscription with a series of (pointwise) local checks on all domain elements and their immediate neighbourhood. Our main positive results are for ontologies in DLs ALCIO and ALCI: we prove that for TBoxes of modal depth 1 (i.e. without nesting of existential or universal quantiﬁers) standard reasoning problems under pointwise circumscription are (co)NEXPTIME-complete and EXPTIMEcomplete, respectively. The restriction of modal depth still yields a large class of ontologies useful in practice, and it is further justiﬁed by a strong undecidability result for pointwise circumscription with general TBoxes in ALCIO.

1 Introduction Description Logics (DLs) are a family of formalisms for Knowledge Representation & Reasoning, speciﬁcally designed for describing entities of a problem domain and their relations in the so-called ontologies [Baader et al., 2017]. Most DLs, including those that underlie the W3C OWL standard ontology languages, are based on ﬁrst-order logic and thus inherit many of its features, including monotonicity. In a monotonic formalism, an inference of a fact from a theory can never be withdrawn, even if new facts become available. This makes it difﬁcult to capture human-like common-sense reasoning, where we may draw default conclusions that can be revised in the light of new information. Consider the following DL knowledge base. It says that margherita (mar) is a pizza that has tomatoes (tmt) and mozzarella (moz) as ingredients, which in turn are vegetarian ingredients. It further states that pizzas whose all ingredients

are vegetarian are vegetarian pizzas.

Pizza(mar) Vegetarian(tmt) Vegetarian(moz)

has Ingredient(mar, tmt) has Ingredient(mar, moz)

Pizza has Ingredient.Vegetarian Vegetarian Pizza

The classical semantics of DLs does not allow us to infer that Margherita is a vegetarian pizza, which might come as a surprise. Indeed, this is because the open-world assumption of classical logic does not rule the existence of some (possibly unidentiﬁed) non-vegetarian ingredient of Margherita. From the perspective of common-sense reasoning, we may want to conclude that a dish only has the ingredients that are explicitly stated or logically implied in the knowledge base, i.e. the extensions of the role has Ingredient should be minimized. Adding non-monotonic features to monotonic formalisms is a big challenge, and it often causes undecidability or a signiﬁcant increase in the complexity of reasoning. Several nonmonotonic extensions of DLs have been proposed, aiming to balance the computational cost and the expressiveness (see, e.g., [Baader and Hollunder, 1995; Donini et al., 1998; Giordano et al., 2013; Britz et al., 2021; Casini et al., 2019; Bonatti et al., 2009]). A prominent research line here is circumscribed DLs [Bonatti et al., 2009; Bonatti et al., 2011; Bonatti et al., 2015; Bonatti, 2021; Bonatti et al., 2022]. Circumscription is a powerful tool that was ﬁrst introduced by Mc Carthy as an extension of ﬁrst-order logic. In the basic setting, the intended (or preferred) models of a circumscribed theory are its classical models that additionally have minimal extensions of some selected predicates [Mc Carthy, 1980; Mc Carthy, 1986; Lifschitz, 1985]. In general, additionally to the minimized predicates, one may specify by means of a circumscription pattern the predicates whose extensions must remain ﬁxed and the predicates that may vary freely during the selection of an intended model. Circumscription captures many use cases for non-monotonic reasoning and can simulate various common-sense reasoning formalisms (see, e.g., [Lin and Zhou, 2011]). Circumscribed DLs are an expressive and versatile family of languages, but unfortunately the complexity of reasoning is often very high, and reasoning is undecidable already in circumscribed ALC if roles are allowed to be minimized. On the other hand, decidability is achieved for fragments of ALCIOQ under the assumption that roles are only

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

varying [Bonatti et al., 2009]. The key reason for the high complexity is the second-order quantiﬁcation that is needed in order to identify the preferred models of a circumscribed 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 quantiﬁcation. We introduce pointwise circumscription in DLs. The basic idea here is to replace the single global minimality check of classical circumscription by multiple local minimality checks at all domain elements and their immediate neighborhood. This opens the way to use algorithmic methods (like the mosaic technique and integer programming) to obtain positive decidability results. This is similar in spirit but orthogonal to the notion introduced by Lifschitz 1986 for ﬁrst-order logic, where the second-order quantiﬁcation over predicate extensions is replaced with a series of additions or removals of tuples in predicates (see the last section for more details). The main contributions of this paper are the following.

We formally deﬁne the notion of pointwise circumscription for DLs. We argue that it yields a useful way to apply a form of the closed-world assumption to DL ontologies and allows to draw intuitive common-sense conclusions from them. Pointwise circumscription is a sound approximation of classic circumscription: if an ontology entails a fact under pointwise circumscription, then the entailment also holds under classic circumscription. The converse does not hold in general, because the more aggressive minimization step of global circumscription allows to discard some classical models that are in turn retained by the pointwise version.

We study the computational complexity of reasoning under pointwise circumscription. Speciﬁcally, we consider standard DL reasoning problems (concept satisﬁability, concept subsumption, and entailment of assertions) for ontologies expressed in (fragments of) the very expressive DL ALCIO. For ontologies with TBoxes of modal depth 1 (i.e. without nesting of existential or universal quantiﬁers) we show (co)NEXPTIME membership results. In the case of ALCI without ABoxes, we have membership in EXPTIME. These results ensure decidability of reasoning in settings that are undecidable under classical circumscription, e.g., with varying concept names, with minimized roles, or with ﬁxed roles. The restriction on quantiﬁer depth still yields a large class of ontologies that is relevant practice (e.g., the popular DLs of the DL-Lite family also disallow nesting of quantiﬁers). The upper bounds are obtained by a sophisticated reduction to integer programming. We also observe that under pointwise circumscription these logics lose the ﬁnite model property that holds under the classical semantics.

The upper bounds above are worst-case optimal; we provide a matching (co)NEXPTIME lower bound for ALCIO by a reduction from an exponential grid tiling problem. Interestingly, the lower bound also applies to ALCI with ABoxes. Finally, as an additional justiﬁcation for the considered syntactic restriction, we provide a strong undecidability result for pointwise circumscription with general TBoxes (of modal depth greater than 1).

Our initial algorithm for concept satisﬁability under pointwise circumscription is presented for concept names only. To lift it to arbitrary concept satisﬁability in Section 4.1, we extend our setting by adding constraints to circumscribed knowledge bases. This appear to be interesting on their own right as an additional tool for ﬂexible yet computationally manageable non-monotonic reasoning in DLs.

2 Preliminaries Here we recall the DL ALCIO. We use NC, NR, and NI to denote countably inﬁnite, mutually disjoint sets of concept names, role names, and individuals. The expression r is the inverse role of a role name r NR. Elements of N + R = NR {r | r NR} are called roles. We let r = r. Given a set R N + R of roles, we let R = {r | r R}. In ALCIO, concepts C are deﬁned using the following grammar:

C := | | A | {a} | C | C C | C C | r.C | r.C

with A NC, r N + R , and a NI. A concept inclusion is an expression of the form C D, where C and D are concepts. An expression of the form A(a), where A NC and a NI, is a concept assertion. An expression of the form r(a, b), with r NR and a, b NI, is a role assertion. A TBox T in ALCIO is a set of concept inclusions, and an ABox A is a set of concept and role assertions. A knowledge base (KB) in ALCIO is a pair K = (T , A), where T is a TBox and A is an ABox. Given a TBox T , we let NC(T ), NR(T ), and NI(T ) denote the sets of concept names, role names, and individual names occurring in T , respectively. We denote with N + C (T ) = NC(T ) {{a} | a NI(T )} { , } the set of basic concepts occurring in T and N + R (T ) = NR(T ) {r | r NR(T )}. Given a concept C in ALCIO, the depth of C, denoted with d(C), is the maximal number of nested quantiﬁers occurring in C, and given a TBox T , the depth of T is the maximal d(C) over all concepts C occurring in T . As usual, the semantics is deﬁned by means of interpretations I = ( I, I) where I is the domain and I the interpretation function. The latter associates to each a NI a unique element a I I, to each A NC a set AI I and to each r NR a set r I I I. The extension of remaining concept and role expressions in ALCIO is deﬁned as usual [Baader et al., 2017]. The notions of a model of an inclusion, a TBox, a KB are also standard. We use M (Γ) to denote the set of models of a TBox or a KB Γ. We say a concept C is satisﬁable w.r.t. a KB K, if CI = holds for some I M (K). We say a concept C is subsumed by a concept D w.r.t. a KB K, if CI DI holds for all I M (K). We say a individual a is an instance of a concept C w.r.t. a KB K, if a I CI holds for all I M (K).

3 Pointwise Circumscription Circumscription whether classical or pointwise extends ﬁrst-order logic with predicate minimization. In the so-called preferred models the extensions of the predicates that are indicated as minimized must be as small as possible, that is, removing any tuple would result in the interpretation not being a model. Other predicates may be forced to remain ﬁxed,

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

Minimal model

S, HG, AA ws chc C, HG

AH AH cj h H h H h H PC

Non-minimal model

S, HG ws chc C, HG

AH AH cj h H h H h H h H

Figure 1: Two comparable models of K C in Example 1 (the signature is abbreviated)

or allowed to vary freely. The speciﬁcation of how to treat each predicate is given by a circumscription pattern. We recall the classic notion of circumscription for DLs, following Bonatti et al. (2009). We denote circumscription patterns as triples P = (M, V, F), where M, V , and F are mutually disjoint subsets of NC NR, respectively standing for minimized, varying, and ﬁxed. If K is a KB and P = (M, V, F) a circumscription pattern such that M, V and F partition the signature of K, we say that K is circumscribed with the pattern P , in symbols Circ P(K). Deﬁnition 1. Let P = (M, V, F) be a circumscription pattern, and assume a pair of interpretations I, J . We write I P J if the following conditions are satisﬁed: (i) I = J and a I = a J for all individuals a, (ii) QI QJ for all Q M, and (iii) QI = QJ for all Q F. We write I P J , if I P J and QI QJ for some Q M. Deﬁnition 2. An interpretation I is a minimal model of Circ P(K), in symbols I |= Circ P(K), if I |= K and there is no interpretation J s.t. J |= K and J P I. We use MM (K, P) to denote the set of minimal models of Circ P(K). Deﬁnition 1 does not restrict in any way how the extension of Q may differ in I and J . It quantiﬁes universally over all subsets of QJ , which may globally drop an arbitrary number of tuples. We introduce a weaker preference relation between interpretations, allowing to compare only structures that differ on at most one point , i.e., one domain element. Deﬁnition 3. Assume a circumscription pattern P and a pair of interpretations I, J . We write I P J , if I P J and there exists e I such that: (i) AI \ {e} = AJ \ {e} for all concept names A, and (ii) r I ( ) = r J ( ) for all role names r, where = I \ {e}. We write I P J , if I P J and QI QJ for some Q M. Deﬁnition 4. An interpretation I is a pointwise minimal model of Circ P(K), in symbols I |= Circ P(K), if I |= K and there is no interpretation J s.t. J |= K and J P I. We use PMM (K, P) to denote the set of pointwise minimal models of Circ P(K). The standard deﬁnitions of concept satisﬁability, concept subsumption, and concept instances are adapted to pointwise minimal models in the obvious way: assume an individual a, concepts C, D, and a circumscribed KB Circ P(K). We write Circ P(K) |= C, if CI = holds for some I

PMM (K, P). We write Circ P(K) |= C D, if CI DI holds for all I PMM (K, P). We write Circ P(K) |= C(a), if a I CI holds for all I PMM (K, P). The aforementioned reasoning tasks can be reduced polynomially one into the other, using an immediate adaptation of the reductions in Bonatti et al.(2009).

Example 1. Consider the KB KC about aquatic animals

Shark(white shark) Crab(caribbean hermit crab) Crab Has Gills Shark Has Gills Has Gills has Habitat.Aqua Habitat Has Gills has Habitat.Aqua Habitat Aqua Animal

circumscribed with the pattern PC = (MC, VC, FC), where MC = {has Habitat}, VC = {Aqua Animal}, and all the other predicates are ﬁxed. Then Circ PC(KC) |= Aqua Animal(white shark), and the same holds for caribbean hermit crab. But if we extend KC into K C by asserting that Caribbean hermit crabs live in the jungle has Habitat(caribbean hermit crab, carib jungle) (they only need water to store in the shell and keep their gills moist) then K C |= Aqua Animal(caribbean hermit crab); the relation |= is indeed non-monotonic. Figure 1 shows two models of K C of which the leftmost one is a preferred model.

In this example global and pointwise circumscription coincide. However, role minimization causes undecidability for the global semantics, while under the pointwise semantics it falls into the decidable fragment we study below. Given a KB K and a circumscription pattern P it is easy to show that MM (K, P) PMM (K, P), hence all logical consequence under pointwise circumscription also follow under global circumscription. The converse does not always hold, as the next example shows.

Example 2. Consider T = {A r.A} circumscribed with P = ({A, r}, , ). Then the interpretation I, where I = {e1, e2}, AI = {e1, e2} and r I = {(e1, e2), (e2, e1)}, is such that I PMM (T , P) and I MM (T , P).

When searching for minimal models, classical circumscription allows for the reconﬁguration of the predicate extensions across the entire model. For instance, if a role is minimized, we may remove arbitrarily many pairs anywhere in the model to obtain a smaller model. Pointwise circumscription allows only for local changes of the extensions: the minimization can only affect a domain element and the roles it participates in, leaving the rest of structure unmodiﬁed. By repeatedly applying such local changes, we can often replicate the minimization across the entire model of classical cir-

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

cumscription, but not always. Speciﬁcally, if there exist cycles in a model, it may be possible to eliminate from the extension of a minimized predicate all objects participating in a cycle at once, while the attempt to eliminate them pointwise, one after another, could lead to a violation of the axioms, as one can see in Example 2. This inability of pointwise circumscription to detect non-minimality in cycles is the core difference with respect to the classical global one. Varying roles also play an important role in the negative computational behaviour of classical circumscription: concept satisﬁability with respect to circumscribed KBs in ALCIO is NEXPNP-complete under classic circumscription, assuming that all roles are varying [Bonatti et al., 2009]. To decide whether a model is minimal, we must consider arbitrary reconﬁgurations of all the varying concepts and roles, across the full model: the non-minimality of a model I may be witnessed by an interpretation J that has a very different structure from I. In contrast, we restrict varying predicates to concepts and do not allow them to vary freely across the model. In this way, to test minimality, it sufﬁces to consider only local modiﬁcations at a single domain element at a time, without allowing to create connections to previously unrelated objects. We prove in the next section that under pointwise circumscription, allowing roles to be minimized or ﬁxed, reasoning is decidable in a very expressive fragment of ALCIO. In contrast, such circumscription patterns lead to undecidability under classical circumscription already in ALC [Bonatti et al., 2009], and the decidability results in the presence of general TBoxes are limited to circumscription patterns with only varying roles. We believe that minimized roles are quite useful in practice and allow to model interesting real-life problems.

4 Decidablity Results

In this section we focus on the fragment of ALCIO where concept expressions have depth at most one, that is, there is no nesting of quantiﬁers. We denote this fragment ALCIOd 1. For our upper bounds, we restrict circumscription patterns by disallowing varying roles, i.e. V NC. We now provide an algorithm for concept name satisﬁability w.r.t. circumscribed TBoxes under pointwise semantics. In this setting, just like in standard ALCIO, reasoning w.r.t (circumscribed) KBs can be polynomial reduced to reasoning w.r.t. (circumscribed) TBoxes: assertions A(b) and r(a, b) can be written as TBox inclusions {a} A and {a} r.{b}, respectively. We start by observing that this restricted fragment is quite expressive and does not have the ﬁnite model property.

Proposition 1. Let G NC. There exists a circumscribed TBox Circ P(T ) in ALCIOd 1 such that each I PMM (T , P) with GI = has an inﬁnite domain.

Proof (sketch). Take the following TBox Tinf :

{a} B B r . C D

p .{a} C r.C1 C1 r .D

C, D C, D C, D C, D G, B

C1, D1 C1, D1 C1, D1

Figure 2: Inﬁnite minimal model contained in every I PMM (Tinf , Pinf ) that satisﬁes G.

D r.D1 D1 r .C p.(C D ({a} (C1 D1))) G

with the circumscription pattern Pinf = (NC(T ) NR(T ), , ). One can show that any model J of Tinf with ﬁnite domain and GJ = is not Pinf - minimal. The interpretation in Figure 2 is an inﬁnite minimal model of this TBox where GI = , and it can be monomorphically embedded in any J MM (Tinf, Pinf) such that GJ = .

Our decidability results are achieved using the mosaic technique [N emeti, 1992]: we show that the existence of a pointwise minimal model can be reduced to checking the existence of a ﬁnite family of fragments of models that can be assembled into a model. The model pieces are called star types and are deﬁned as pairs (T, ρ) where T describes the set of concepts that hold at a domain element, while ρ stores the description of the neighbourhood of the element described by T. We call spikes the elements of ρ. We need to ﬁnd a multiplicity function N telling us how many copies of each star type we should take to guarantee that a model in PMM (T , P) can be built. To make sure that the model is pointwise minimal we impose local minimality conditions on the star types, and we also need to do some book-keeping to guarantee that the minimality is preserved while assembling the model. Hence each spike in ρ not only describes the local neighbourhood of a node, but also includes two labelling functions that keep track of the justiﬁcations for some predicates. We assume TBoxes in negation normal form (NNF). Given a concept C, we denote with C the negation normal form of C. Given a TBox T , the closure of T , denoted with cl(T ), is the smallest subset of concepts containing every concept in T that is closed under subconcepts and negations (in NNF). Given a concept C, cl(C) denotes the closure of C and it is deﬁned analogously to the closure of a TBox. Deﬁnition 5. Given a TBox T , a concept-type is a subset T cl(T ) such that: (i) if C D T , then C T or D T; (ii) C T if and only if C T; (iii) if C1 C2 T, then C1 T or C2 T; (iv) if C1 C2 T, then {C1, C2} T. Types(T ) denotes the set of all concept-types T with T. Given a concept-type T Types(T ) and a concept C T, we say that C is forced in T if T Types(T ) where T is obtained from T by (1) removing C and any C1 Cn, with Ci = C, for some i n, and (2) adding

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

C and (C1 Cn), for any removed conjunction. When labelling spikes, forced concepts allow us to correctly identify when a concept r.C is necessary for the local consistency of the star type and uniquely represented in the spike. Now we formally deﬁne star types. To enhance readability, we denote with r a role or an inverse of a role, i.e. r NR or r = t , with t NR. If r = t , then r denotes t. For any concept D, we denote with sub(D) the set of all (sub)concepts occurring in D. Given a TBox T , we deﬁne the set of labels

LT = { r.B sub( C D)| C D T }.

By N we denote the set of extended natural numbers N {0, } with the usual sum and product operations. A multiset S is a pair S = (A, m S), where A is a set of elements, called support set, and m S : A N \ {0} is a function associating to each element of A its multiplicity. Given a multiset S, we use supp(S) to denote the support of S. We denote with |S| the cardinality of the multiset, given by the sum of the multiplicities of its elements. Given a multiset S such that m S(e) < , for any e supp(S) we deﬁne the set Sm = {(e, j)|e supp(S) 0 < j m S(e)}. Deﬁnition 6. Assume a TBox T in ALCIOd 1. A star type is a pair (T, ρ) where (a) T Types(T ), (b) ρ is a multiset where supp(ρ) is a set ofspikes s = (Rs, Ts, Ls, L s ) such that Rs N + R (T ), Ts Types(T ) and Ls, L s LT . A star type (T, ρ) is suitable for T if the following conditions are satisﬁed: (1) |ρ| is ﬁnite; (2) If r.B T then there exists s supp(ρ) such that r Rs and B Ts; (3) If r.B T then for all s supp(ρ) such that r Rs, B Ts; (4) For all s supp(ρ), if r.B Ts and r R s then B T. For each s supp(ρ) the labellings Ls and L s are as follows: (5) r.B Ls if and only if (a) r.B T, r Rs and B Ts, and there is no s supp(ρ) s.t. s = s, r Rs and B Ts , (b) mρ(s) = 1, (c) r.B is forced in T. (6) r.B L s only if r.B Ts, r R s and B Ts. We shortly discuss the conditions above. Condition (1) ensures that the number of spikes in a star type is bounded, and will be important to keep the number of star types small ; conditions (2)-(4) ensure that the star type represents a fragment of a model of a given TBox; condition (5) and (6) deal with the content of the labelling sets Ls and L s , of a given spike s. The set Ls stores exactly those existentials in T that have its unique and necessary witness in s. In particular, condition (c) is relevant, as a concept-type T might contain arbitrary disjunctions of concepts of the form r.C such that each of the existentials is uniquely represented by a spike, but might not be necessary for the local consistency of the

type. The role of L s is a bit more involved and related to the conditions in Theorem 1: it allows us to mark existential concepts in Ts that may not be minimally satisﬁed at the current T, but which are necessary when we append another star type at s whose labelling is coherent with L s . We say a star type (T, ρ) is k-bounded if |ρ| k. We denote by T(T ) the set of all star types suitable for T , and by Tk(T ) those that are k-bounded. We deﬁne a minimality condition on star types reﬂecting P minimality. Let R+ = R R .

Deﬁnition 7. Given P = (M, V, F) and (T, ρ), (T , ρ ) Tk(T ), we say that (T, ρ) P (T , ρ ) if

(i) M T M T and F T = F T ,

(ii) there exists a bijection f : ρm ρ m associating to each (s, i) ρm an element f(s, i) = (s , j) ρ m s. t.:

M R+ s M R+ s and F R+ s = F R+ s ,

Ts = Ts and L s = L s .

We say that (T, ρ) <P (T , ρ ) if M T M T or M R+ s M R+ s , for some s supp(ρ) with f(s, i) = (s , j). A star type (T, ρ) is minimal if there exists no (T , ρ ) such that (T , ρ ) <P (T, ρ).

We denote by Tmin(T , P) the set of all star types in T(T ) that are minimal given P, and by Tmin k (T , P) those that are additionally k-bounded.

Deﬁnition 8. Assume two star types (T, ρ), (T , ρ ) T(T ). Given a spike s supp(ρ), such that s = (Rs, T , Ls, ), we say that ρ is compatible with s if for any r R s and B T such that r.B T , there is no s supp(ρ ) with r.B Ls .

A star type (T, ρ) can be extended with a spike s = (Rs, Ts, Ls, L s ). Let ρ be the multiset with support supp(ρ) {s}. The multiplicity function mρ is as follows: if there exists s supp(ρ) with s = s, then mρ (s) = mρ(s )+1, otherwise mρ (s) = 1; for all s supp(ρ) with s = s, mρ (s ) = mρ(s ). We denote with (T, ρ) + s the result of the extension. Given a star type (T, ρ) and a spike s = (R, T , L, L ) supp(ρ), we call inverse of s the spike s = (R , T, L , L).

Lemma 1. Assume (T, ρ), (T , ρ ) Tmin(T , P). For any s supp(ρ) with s = (Rs, T , Ls, ), if ρ is compatible with s, then (T , ρ ) + s is also in Tmin(T , P).

The following conditions on the multiplicity function N ensure that we can assemble a model. They are analogous to those in [Gogacz et al., 2020a], but account also for pointwise minimality. Given a TBox T , let T = |cl(T )|.

Theorem 1. Let P = (M, V, F) be a circumscription pattern with V NR = . Consider a TBox T in ALCIOd 1 and a concept name C0. Let n := 5 T , the following are equivalent:

(i) There exist I PMM (T , P) such that CI 0 = ;

(ii) There exists a function N : Tmin n (T , P) N such that the following conditions are satisﬁed:

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

(1) For all a NI(T ), X

(T,ρ) Tmin n (T ,P) {a} T

N((T, ρ)) = 1

(T,ρ) Tmin n (T ,P) C0 T

N((T, ρ)) 1

(3) For all T, T Types(T ), R N + R and L, L LT with L = , X

(T,ρ) Tmin n (T ,P) s=(R,T ,L,L ) supp(ρ)

mρ(s) N(T, ρ) X

(T ,ρ ) Tmin n (T ,P) s supp(ρ )

(4) For all T, T Types(T ), R N + R and L LT , X

(T,ρ) Tmin n (T ,P) s=(R,T ,L, ) supp(ρ)

N(T, ρ) > 0 implies X

(T ,ρ ) Tmin n (T ,P) and ρ compatible with s

N(T , ρ ) > 0.

Let us brieﬂy discuss the conditions (1)-(4) above: (1) ensures that each nominal is instantiated only once; (2) ensures the satisfaction of C0; (3) implies that for each spike with L = there exists at least one star type having the inverse of the spike in its set of spikes (intuitively this allows an overlapping between the spikes and preserves the meaning of the labelling sets); (4) ensures that, for each spike such that L = has a compatible star type, i.e. such that the resulting extended star type is minimal. Following Gogacz et al.(2020a; 2020b), we use a system of inequalities to ﬁnd the function N. A system of linear inequalities is a pair (V, E), where V is a set of variables and E is a set of linear inequalities of the form a1x1 + +anxn + c b1y1 + + bmym, where a1, . . . , an, b1, . . . , bm N, c Z, {x1, . . . , xn, y1, . . . , ym} V . If c 0 the inequality is called positive. We call extended system of inequalities any system (V, E, I) where (V, E) is a system of linear inequalities and I is a set of implications x1 + + xn > 0 y1 + + ym > 0, with x1, . . . , xn, y1, . . . , ym V . By introducing for each (T, ρ) a variable x(T,ρ), the conditions (1)-(4) can be transformed into an extended system (V, E, I) such that a solution S corresponds to a function N : Tmin n (T , P) N satisfying (1)-(4), and vice versa. Given an extended system (V, E, I) in which all the coefﬁcients are in the integers in the interval [ a, a] for some a N, the existence of a solution S for H can be decided in non-deterministic polynomial time in |V | + |E| + |I| + a [Gogacz et al., 2020a]. If the system contains only positive inequalities, the existence of a solution can be decided in deterministic polynomial time [Lutz et al., 2005]. The aforementioned results apply in the settings of Theorem 1, as the only coefﬁcients greater than 1 result from (3). Since the multiplicity of each spike is bounded by 5 T , all the coefﬁcients of the system of inequalities are in the interval [ 5 T , 5 T ]. Theorem 2. For ALCIOd 1 KBs, concept name satisﬁability under pointwise circumscription is in NEXPTIME if all roles are either minimized or ﬁxed.

The upper bound of Theorem 2 is tight: following the idea of [Tobies, 2000] we can reduce the exponential grid tiling problem to concept satisﬁability w.r.t. circumscribed KBs in ALCId 1 under the pointwise semantics.

Theorem 3. For ALCId 1 KBs, concept name satisﬁability under pointwise circumscription is NEXPTIME-hard.

Crucially, the hardness proof uses one individual and ABox assertions (which in ALCI cannot be internalized in the TBox). If there are no individuals, we can drop (1) in Theorem 1 and obtain a positive extended system of inequalities. The matching lower bound is inherited from (classical) ALC [Schild, 1991].

Corollary 1. For ALCId 1 TBoxes, concept name satisﬁability under pointwise circumscription is in EXPTIMEcomplete if all roles are either minimized or ﬁxed.

4.1 Constraints for General Concept Satiﬁability In this section we lift our results from concept names to arbitrary concepts. Classically, this can be done introducing new axioms to the TBox. However, under pointwise circumscription this affects the semantics.

Example 3. Consider the TBox T = {A r.B, B r.C} and the circumscription pattern P = (M, V, F) with M = {C} and F = {A, B, r}. Consider the concept C0 = r. r.C. We extend T with the TBox TC0 = {D0 r. r.C}, reducing checking the satisﬁability of C0 to checking the satisﬁability of D0. The circumscription pattern P can be extended to P = (M, V {D0}, F). Consider the interpretation I such that I = {a, b, c} and r I = {(a, b), (b, c)}, AI = BI = , DI 0 = {a}, and CI = {c}. It is easy to see that I PMM (T TC0, P ). However, I PMM (T , P) where I is the model of T obtained from I restricting it to the syntax of T and C0. Putting D0 into M or F instead does not preserve the semantics either. For the case where D0 M, consider J = {a, b, c}, DJ 0 = {a}, AJ = {a}, BJ = {b}, CJ = {a, b, c} and r J = {(a, b), (b, c)}. Then D0 can be minimized at a. In contrast, the model J obtained from J restricting it to the syntax of T and C0 is minimal.

Given a concept C0 with d(C0) > 0 and a circumscribed TBox Circ P(T ) in ALCIOd 1, checking the satisﬁability of C0 in a minimal model of T has no inﬂuence on the minimality of the model itself. We use constraints to ﬁlter out those models that do not satisfy a given concept C0. A constraint set C is a collection of pairs of concepts (C, D), with the intuitive meaning if C holds, then D must hold too . The pair (T , C) denotes a TBox T equipped with a constraint set C. Given a circumscription pattern P we denote with Circ P(T , C) a circumscribed TBox T equipped with a set of constraints C.

Deﬁnition 9. Given a KB K, a set of constraints C and a circumscription pattern P, we say that an interpretation I is a model of Circ P(K, C), in symbols I |= Circ P(K, C), if I |= Circ P(K), and CI DI, for all (C, D) C.

Given Circ P(K, C) we denote with PMM (K, C, P) the set of all interpretations I such that I |= Circ P(K, C).

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

Although classically constraints behave as axioms, under the (pointwise) circumscription setting constraints represent a further level of expressiveness. This key aspect is underlined in the example below. Example 4. Assume that we want to describe the following scenario. Administrators can grant to users access to classiﬁed ﬁles. If a classiﬁed ﬁle is read, the permission to do so should have been granted. Consider the knowledge base K

Classiﬁed Document(f1) User(John) read(John, f1) access granted by.Admin Has Read Permission

Consider the constraint set C with the unique constraint

(Classiﬁed Document, (read) .Has Read Permission)

circumscribed with M = {Has Read permission} and keeping all the other predicates ﬁxed. The constraint imposes that whenever a classiﬁed document is read, the user reading it has permission to do so, and this permission is granted by an Admin, as the concept Has Read permission is minimized. Thus, in any minimal model of (K, C) we have that John is an instance of Has Read Permition access granted by.Admin. Counterintuitively, if we replace the constraint with the axiom

Classiﬁed Document (read) .Has Read Permission

we can derive that John has permission to read f1 without the approval of an administrator. We can introduce a constraint to reduce general concept satisﬁability to satisﬁability of a concept name. Proposition 2. Assume a circumscription pattern P = (M, V, F), a TBox T and a concept C0 in ALCIO of arbitrary depth. The following are equivalent: (i) I PMM (T , P) such that CI 0 = ,

(ii) I PMM (T , C, P ) such that C 0 I = , with C = {(C 0, C0)}, C 0 concept name not occurring in T and P = (M, V {C 0}, F). To adapt our mosaic technique to constraints, we ﬁrst reduce their depth. The depth of a constraint C, denoted with d(C), is the maximum of the depths of the concepts occurring in C. Observe that the constraint set C of Proposition 2 has the same depth as C0. A constraint set C of depth n can be transformed in a constraint set C of depth n 1 applying the following steps: (CN1) For each (C, D) C, introduce a fresh symbol Di for each sub-concept Bi with d(Bi) = 1, with i k N, (CN2) Build the constraint set C , (a) replacing each occurrence of Bi in D with Di, (b) adding the constraint (Di, Bi), if Bi in D, or (Bi, Di), if Bi in C, for each i k. Iteratively applying (CN1)-(CN2), a constraint set of arbitrary depth can be reduced to depth 1. Proposition 3. Assume Circ P(T , C) with P = (M, V, F) and d(C) > 1, and a concept C0. Let C be the constraint set obtained from C applying (CN1)-(CN2) until d(C ) = 1, and let H be the set of fresh concept names introduced. Let P = (M, V H, F). The following are equivalent:

h. v. r.{a} (1)

t T,t =t At ) (2)

(t,t ) H h.At ) (3)

(t,t ) V v.At ) (4)

A B (5) A P.B P. P.B (6)

B P .A P . P .A (7)

r .(A B) G (8)

Figure 3: The TBox TP : P abbreviates h v h v and P

abbreviates v h v h .

(i) I PMM (T , C, P) such that CI 0 = ,

(ii) I PMM (T , C , P ) such that CI 0 = ,

Star types can be required to satisfy a given set of constraints, provided that they have depth at most 1. Given a constraint set C, cl(C) denotes the closure of C and is deﬁned analogously to the closure of a TBox. Let Types(T , C) denotes the set of T cl(T ) cl(C) satisfying (i)-(iv) of Deﬁnition 5 such that T.

Deﬁnition 10. Given a TBox T in ALCIOd 1 and a set of constraints C with d(C) 1, a star type (T, ρ) is suitable for (T , C) if T Types(T , C), (T, ρ) is suitable for T , and for each (C, D) C, if C T then D T.

Given a TBox T , a set of constraints C and a circumscription pattern P, we denote with Tmin k (T , C, P) the set of all k-bounded minimal (w.r.t. P) star types (T, ρ), suitable for (T , C). Given a constraint set C, let C = |cl(C)|.

Theorem 4. Assume a circumscription pattern P, a TBox T and set of constraints C in ALCIOd 1. Let m = 5 T + C . Given a concept name C0, the following are equivalent:

(i) there exists I PMM (T , C, P) such that CI 0 = ,

(ii) there exists N : Tmin m (T , C, P) N , satisfying conditions (1)-(4) in Theorem 1.

Corollary 2. Under pointwise circumscription, if all roles are either minimized or ﬁxed, general concept satisﬁability is

NEXPTIME-complete for ALCIOd 1 TBoxes and KBs,

EXPTIME-complete for ALCId 1 TBoxes.

5 Undecidability Result

Can we drop our restriction to TBoxes of depth one? Under the classical semantics, and also under global circumscription we can normalize TBoxes of arbitrary depth into TBoxes of depth one. However, under pointwise circumscription, the usual normalization does not preserve the semantics.

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

Example 5. Consider the TBox T = {A r. r.B} with the circumscription pattern P = (M, V, F) with M = {A, B} and F = {r}, and assume we want to check the satisﬁability of B w.r.t. Circ P(T ). Applying a naive form of normalization, renaming complex expressions with fresh concept names, we obtain the TBox TN = {A r.C0, C0 r.B}. Consider the circumscription pattern PN = (M, V {C0}, F). The interpretation IN such that IN = {e1, e2}, CI 0 = {e1}, BI = {e2} and r I = {(e1, e2)} is a pointwise minimal model of Circ PN(TN), i.e. IN PMM (TN, PN), such that BIN = . However, the interpretation I obtained restricting IN to the signature of T is not a pointwise minimal model of Circ P(T ). One can further observe that there exists no I PMM (T , P) such that BI = . Putting C0 into M or F does not preserve the semantics either. Looking for more sophisticated forms of normalization is futile. With a reduction from the domino problem, we prove that under the pointwise semantics reasoning w.r.t. circumscribed ALCIO TBoxes of unbounded depth is undecidable. An instance of the domino problem is a triple P = (T, H, V ), where T is a set of tiles, H, V T T are the horizontal and vertical matchings between tiles. A solution for P is a map τ : N N T such that, for each i, j N: (τ(i, j), τ(i + 1, j)) H, and (τ(i, j), τ(i, j + 1)) V . Consider the TBox TP in Figure 3, with the circumscription pattern P such that M = NC(T ) NR(T ). Lemma 2. P has a solution if and only if there exists I PMM (TP , P) such that GI = . We use the spy-point technique (1). Axioms (5)-(8) enforce the grid. In particular: axiom (5) ensures that each node is labelled with A or B; axiom (8) implies that (in a minimal model where G is satisﬁed) A and B are satisﬁed at every point; axioms (6) and (7), together with the minimization of h and v, enforce that there exists a unique hvh v path and a unique vhv h path to each element. Theorem 5. Reasoning w.r.t general TBoxes in pointwise circumscribed ALCIO is undecidable. As mentioned, the reduction uses the spy-point technique, which requires nominals. Thus, it does not easily carry over ALCI. The problem of establishing the decidability (or undecidability) of reasoning w.r.t. pointwise circumscribed ALCI general KBs is left open.

6 Discussion and Future Work In this paper, we have proposed a new notion of circumscription for DLs with the aim of obtaining an expressive DLbased framework for non-monotonic reasoning that circumvents the undecidability problems of classic circumscription. E.g., to show that standard reasoning problems under pointwise circumscription in ALCIO are in (co)Nexp Time it sufﬁces to impose two restrictions: limiting quantiﬁer depth to 1, and disallowing varying roles. Such restrictions do not sufﬁce for ensuring decidability in classic circumscription. Moreover, even for fragments where both semantics are decidable, our framework has lower complexity.

The term pointwise circumscription was ﬁrst coined by Lifschitz (1986) who proposed a similar framework for ﬁrstorder logic. The basic idea there is to replace the secondorder quantiﬁcation of classic circumscription with a (possibly inﬁnite) conjunction of minimality tests for all tuples of domain elements that participate in relations; each test veriﬁes the impossibility of removing the tuple from a relation while preserving a model of the input theory. Moreover, in Lifschitz s setting, second-order quantiﬁcation is used for varying predicates. That form of circumscription is orthogonal to ours: a point in the former corresponds to a single tuple in a relation, while in this paper a point means an object in a structure, and the minimality check concerns the possibility of improving the structure by changing the concept names or the roles that the object participates in. There are several directions for future work. A natural next step is to study the computational impact of varying roles. We believe that they do not cause an increase in complexity for ALCIO, but the algorithm becomes more involved, requiring a more complex notion of star types and an additional condition in point (ii) of Theorem 1. We want to study pointwise circumscription with priorities (as a generalization of parallel circumscription here), and to further study the constraints introduced in Section 4.1, which seem to provide additional expressiveness at little computational cost. We are also investigating syntactic restrictions on ontologies such as acyclicity notions to ensure that pointwise and global circumscription coincide. We stress that the two semantics coincide for all our knowledge representation examples, and we had to use an artiﬁcial example to stress the differences. This gives us hope that, in practice, it will rarely be relevant that in our semantics minimization is weaker than in global circumscription. We plan to study rewritings of pointwise circumscribed ontologies into ontologies under the standard semantics, thus enabling reuse of existing efﬁcient reasoners. Finally, we want to extend our investigation to further extensions of ALCI, e.g., with role hierarchies, and qualiﬁed number restrictions.

Acknowledgements This work was partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation. It was also partially supported by the Austrian Science Fund (FWF) projects P30360, P30873 and W1255, and by the Vienna Business Agency s project Co Rec.

References [Baader and Hollunder, 1995] F. Baader and B. Hollunder. Priorities on defaults with prerequisites, and their application in treating speciﬁcity in terminological default logic. Journal of Automated Reasoning, 15(1):41 68, 1995. [Baader et al., 2017] F. Baader, I. Horrocks, C. Lutz, and U. Sattler. An Introduction to Description Logic. Cambridge University Press, Cambridge, UK, 2017. [Bonatti et al., 2009] Piero A. Bonatti, Carsten Lutz, and Frank Wolter. The complexity of circumscription in description logic. Journal of Artiﬁcial Intelligence Research, (35):717 773, September 2009.

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)

[Bonatti et al., 2011] Piero A. Bonatti, Marco Faella, and Luigi Sauro. Defeasible inclusions in low-complexity DLs. J. Artif. Intell. Res., 42:719 764, 2011. [Bonatti et al., 2015] Piero A. Bonatti, Marco Faella, Carsten Lutz, Luigi Sauro, and Frank Wolter. Decidability of circumscribed description logics revisited. In Thomas Eiter, Hannes Strass, Miroslaw Truszczynski, and Stefan Woltran, editors, Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation - Essays Dedicated to Gerhard Brewka on the Occasion of His 60th Birthday, volume 9060 of Lecture Notes in Computer Science, pages 112 124. Springer, 2015. [Bonatti et al., 2022] P.A. Bonatti, I.M. Petrova, and L. Sauro. Optimizing the computation of overriding in dln. Artiﬁcial Intelligence, 311:103764, 2022. [Bonatti, 2021] Piero A. Bonatti. Query answering in circumscribed OWL2 proﬁles. Ann. Math. Artif. Intell., 89(12):1155 1173, 2021. [Britz et al., 2021] Katarina Britz, Giovanni Casini, Thomas Meyer, Kody Moodley, Uli Sattler, and Ivan Varzinczak. Principles of KLM-style defeasible description logics. ACM Trans. Comput. Log., 22(1):1:1 1:46, 2021. [Casini et al., 2019] Giovanni Casini, Umberto Straccia, and Thomas Meyer. A polynomial time subsumption algorithm for nominal safe ELO under rational closure. Information Sciences, 501:588 620, 2019. [Donini et al., 1998] F.M. Donini, M. Lenzerini, D. Nardi, W. Nutt, and A. Schaerf. An epistemic operator for description logics. Artiﬁcial Intelligence, 100(1):225 274, 1998. [Giordano et al., 2013] L. Giordano, V. Gliozzi, N. Olivetti, and G.L. Pozzato. A non-monotonic description logic for reasoning about typicality. Artiﬁcial Intelligence, 195:165 202, 2013. [Gogacz et al., 2020a] Tomasz Gogacz, V ıctor Guti errez Basulto, Yazm ın Ib a nez-Garc ıa, Filip Murlak, Magdalena Ortiz, and Mantas Simkus. Ontology focusing: Knowledge-enriched databases on demand. In ECAI 2020 - 24th European Conference on Artiﬁcial Intelligence, volume 325 of Frontiers in Artiﬁcial Intelligence and Applications, pages 745 752. IOS Press, 2020. [Gogacz et al., 2020b] Tomasz Gogacz, Sanja Lukumbuzya, Magdalena Ortiz, and Mantas Simkus. Datalog rewritability and data complexity of ALCHOIF with closed predicates. In Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pages 434 444, 2020. [Lifschitz, 1985] V. Lifschitz. Closed-world databases and circumscription. Artiﬁcial Intelligence, 27(2):229 235, 1985. [Lifschitz, 1986] Vladimir Lifschitz. Pointwise circumscription: Preliminary report. In Proceedings of the Fifth AAAI National Conference on Artiﬁcial Intelligence, AAAI 86, pages 406 410. AAAI Press, 1986.

[Lin and Zhou, 2011] Fangzhen Lin and Yi Zhou. From answer set logic programming to circumscription via logic of GK. Artif. Intell., 175(1):264 277, 2011. [Lutz et al., 2005] Carsten Lutz, Ulrike Sattler, and Lidia Tendera. The complexity of ﬁnite model reasoning in description logics. Information and Computation, 199(1):132 171, 2005. 19th International Conference on Automated Deduction (CADE-19). [Mc Carthy, 1980] J. Mc Carthy. Circumscription a form of non-monotonic reasoning. Artiﬁcial Intelligence, 13(1):27 39, 1980. Special Issue on Non-Monotonic Logic. [Mc Carthy, 1986] J. Mc Carthy. Applications of circumscription to formalizing common-sense knowledge. Artiﬁcial Intelligence, 28(1):89 116, 1986. [N emeti, 1992] I. N emeti. Decidable versions of ﬁrst order logic and cylindric-relativized set algebras. In CSLI Publications, editor, Logic Colloquium 92, pages 171 241, 1992. [Schild, 1991] Klaus Schild. A correspondence theory for terminological logics: Preliminary report. In John Mylopoulos and Raymond Reiter, editors, Proc. of the 12th Int. Joint Conf. on Artiﬁcial Intelligence (IJCAI 1991), pages 466 471. Morgan Kaufmann, 1991. [Tobies, 2000] Stephan Tobies. The complexity of reasoning with cardinality restrictions and nominals in expressive description logics. Journal of Artiﬁcial Intelligence Research, (12):199 217, 2000.

Proceedings of the Thirty-Second International Joint Conference on Artiﬁcial Intelligence (IJCAI-23)