Description Logics with Pointwise Circumscription

1 Introduction

Description Logics (DLs) are a family of formalisms for Knowledge Representation & Reasoning, specifically 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 first-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 difficult 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)

hasIngredient(mar, tmt) hasIngredient(mar,moz)

Pizza ⊓ ∀hasIngredient.Vegetarian ⊑ VegetarianPizza

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 unidentified) 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 hasIngredient should be minimized.

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 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 first introduced by McCarthy as an extension of first-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 [McCarthy, 1980; McCarthy, 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 fixed 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 varying [Bonatti et al., 2009]. 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 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 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 first-order logic, where the second-order quantification 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 define 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. Specifically, we consider standard DL reasoning problems (concept satisfiability, 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 quantifiers) 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 fixed roles. The restriction on quantifier 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 quantifiers). The upper bounds are obtained by a sophisticated reduction to integer programming. We also observe that under pointwise circumscription these logics lose the finite 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 justification 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 satisfiability under pointwise circumscription is presented for concept names only. To lift it to arbitrary concept satisfiability 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 flexible 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 infinite, 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 defined using the following grammar:

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 quantifiers 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 defined 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 aI ∈ ∆I , to each A ∈ NC a set AI ⊆ ∆I and to each r ∈ NR a set rI ⊆ ∆I ×∆I . The extension of remaining concept and role expressions in ALCIO is defined 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 satisfiable w.r.t. a KB K, if C I ̸= ∅ holds for some I ∈ M(K). We say a concept C is subsumed by a concept D w.r.t. a KB K, if C I ⊆ 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 aI ∈ C I holds for all I ∈ M(K).

3 Pointwise Circumscription

Circumscription-whether classical or pointwise-extends first-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 fixed,

Minimal model

Non-minimal model

or allowed to vary freely. The specification 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 fixed. 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 CircP(K).

Definition 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 satisfied:

(i) ∆I =∆J and aI = aJ 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.

Definition 2. An interpretation I is a minimal model of CircP(K), in symbols I |= CircP(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 CircP(K).

Definition 1 does not restrict in any way how the extension of Q may differ in I and J . It quantifies 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.

Definition 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:

We write I ≺·P J , if I ⪯·P J and QI ⊂QJ for some Q∈M. Definition 4. An interpretation I is a pointwise minimal model of CircP(K), in symbols I |=· CircP(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 CircP(K).

The standard definitions of concept satisfiability, 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 CircP(K). We write CircP(K) |=· C, if C I ̸= ∅ holds for some I ∈

PMM(K, P). We write CircP(K) |=· C ⊑ D, if C I ⊆ DI holds for all I ∈ PMM(K,P). We write CircP(K) |=· C(a), if aI ∈ C I 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 ⊑ HasGills Shark ⊑ HasGills

HasGills ⊑ ∃hasHabitat.AquaHabitat

HasGills ⊓ ∀hasHabitat.AquaHabitat ⊑ AquaAnimal

circumscribed with the pattern PC = (MC, VC, FC), where MC = {hasHabitat}, VC = {AquaAnimal}, and all the other predicates are fixed. Then CircPC (KC) |=· AquaAnimal(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 hasHabitat(caribbean hermit crab, carib jungle) (they only need water to store in the shell and keep their gills moist) then K′C ̸|=· AquaAnimal(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 rI = {(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 reconfiguration 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 unmodified. By repeatedly applying such local changes, we can often replicate the minimization across the entire model of classical circumscription, but not always. Specifically, 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 satisfiability with respect to circumscribed KBs in ALCIO is NEXP NP -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 reconfigurations 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 suffices to consider only local modifications 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 fixed, 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 quantifiers. 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 satisfiability 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 finite model property.

Proposition 1. Let G ∈ NC. There exists a circumscribed TBox CircP(T ) in ALCIOd≤1 such that each I ∈ PMM(T , P) with GI ̸= ∅ has an infinite domain.

Proof (sketch). Take the following TBox Tinf :

with the circumscription pattern Pinf = (NC(T ) ∪ NR(T ), ∅, ∅). One can show that any model J of Tinf with finite domain and GJ ̸= ∅ is not ≺·Pinf -minimal. The interpretation in Figure 2 is an infinite 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 finite family of 'fragments' of models that can be 'assembled' into a model. The model pieces are called star types and are defined 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 find 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 justifications 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 defined analogously to the closure of a TBox.

Definition 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

∼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 define 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 define the set of labels

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, mS), where A is a set of elements, called support set, and mS : 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 mS(e) < ∞, for any e ∈ supp(S) we define the set Sm = {(e, j)|e ∈ supp(S) ∧ 0 < j ≤ mS(e)}.

Definition 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 of spikes 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 satisfied:

1. |ρ| is finite;
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 ∈ Rs then B ∈ T.

For each s ∈ supp(ρ) the labellings Ls and L-s are as follows:

1. ∃r.B ∈ Ls if and only if
2. (a) ∃r.B ∈ T, r ∈ Rs and B ∈ Ts, and there is no s′ ∈ supp(ρ) s.t. s′ ̸= s, r ∈ Rs′ and B ∈ Ts′ ,
3. (b) mρ(s) = 1,
4. (c) ∃r.B is forced in T.
5. ∃r.B ∈ L-s only if ∃r.B ∈ Ts, r ∈ Rs 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 satisfied 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 define a minimality condition on star types reflecting ≺·P minimality. Let R+ = R ∪ R-.

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

Definition 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 ∈ Rs 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 C I 0 ̸= ∅;
• (ii) There exists a function N : Tmin n (T ,P) →N∗ such that the following conditions are satisfied:

Let us briefly 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 find 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 coefficients 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 coefficients greater than 1 result from (3). Since the multiplicity of each spike is bounded by 5‖T ‖, all the coefficients of the system of inequalities are in the interval [-5‖T ‖, 5‖T ‖].

Theorem 2. For ALCIOd≤1 KBs, concept name satisfiability under pointwise circumscription is in NEXPTIME if all roles are either minimized or fixed.

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

Theorem 3. For ALCId≤1 KBs, concept name satisfiability 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 satisfiability under pointwise circumscription is in EXPTIMEcomplete if all roles are either minimized or fixed.

4.1 Constraints for General Concept Satifiability

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 satisfiability of C0 to checking the satisfiability 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 rI = {(a, b), (b, c)}, AI = BI = ∅, DI 0 = {a}, and C I = {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}, C J = {a, b, c} and rJ = {(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 CircP(T ) in ALCIOd≤1, checking the satisfiability of C0 in a minimal model of T has no influence on the minimality of the model itself. We use constraints to filter 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 CircP(T , C) a circumscribed TBox T equipped with a set of constraints C.

Definition 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 CircP(K, C), in symbols I |=· CircP(K, C), if I |=· CircP(K), and C I ⊆DI , for all (C,D) ∈ C.

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

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 classified files. If a classified file is read, the permission to do so should have been granted. Consider the knowledge base K

Classified Document(f1) User(John) read(John, f1) ∃access granted by.Admin ⊑ Has Read Permission

Consider the constraint set C with the unique constraint

(Classified Document, ∀(read)-.Has Read Permission)

circumscribed with M = {Has Read permission} and keeping all the other predicates fixed. The constraint imposes that whenever a classified 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

Classified 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 satisfiability to satisfiability 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 C I 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 first 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 CircP(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:

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 C I 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 defined analogously to the closure of a TBox. Let Types(T , C) denotes the set of T ⊆ cl(T ) ∪ cl(C) satisfying (i)-(iv) of Definition 5 such that ⊥ ̸∈ T .

Definition 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 C I 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 fixed, general concept satisfiability 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.

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 satisfiability of B w.r.t. CircP(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}, C I 0 = {e1}, BI = {e2} and rI = {(e1, e2)} is a pointwise minimal model of CircPN (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 CircP(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 satisfied) A and B are satisfied 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 FutureWork

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)NexpTime it suffices to impose two restrictions: limiting quantifier depth to 1, and disallowing varying roles. Such restrictions do not suffice 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 first coined by Lifschitz (1986) who proposed a similar framework for firstorder logic. The basic idea there is to replace the secondorder quantification of classic circumscription with a (possibly infinite) conjunction of minimality tests for all tuples of domain elements that participate in relations; each test verifies the impossibility of removing the tuple from a relation while preserving a model of the input theory. Moreover, in Lifschitz's setting, second-order quantification 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 artificial 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 efficient reasoners. Finally, we want to extend our investigation to further extensions of ALCI, e.g., with role hierarchies, and qualified 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 CoRec.