Circumscription in DL-Lite: Progress Report

Abstract

Circumscription is a prominent approach to bring non-monotonicity to Description Logics (DLs), but unfortunately, it usually displays very high computational complexity of reasoning. Many works have studied circumscribed DLs, but most of them focus on expressive DLs containing ℒ, and the results for low-complexity DLs are limited. This paper summarises some recent progress in characterizing the computational complexity of reasoning in circumscribed DL-Lite. We perform a two-dimensional analysis, considering diferent languages of the DL-Lite family, and varying how concepts and roles are treated. In addition to classical circumscription, we consider the recently studied pointwise circumscription, which shows better complexity, in some cases, and remains decidable in the presence of minimized roles.

Keywords

• eol>Circumscription
• Non-monotonic reasoning
• DL-Lite
• Lightweight DLs
• Computational Complexity

1. Introduction

As decidable fragments of first-order logic, Description Logics (DLs) are intrinsically monotonic and do not allow to perform commonsense reasoning. To overcome this limitation, several non-monotonic extensions of DLs have been proposed [ 1, 2, 3, 4, 5 ]. A prominent research line here is given by circumscribed DLs [ 6, 7, 8, 9, 10 ].

Circumscription, as originally introduced by McCarthy to formalize commonsense reasoning [ 11 ], extends first-order logic with the ability to minimize predicate extensions. Later it was extended to allow fixed and varying predicates [ 12 ]; a so-called circumscription pattern specifies how predicates are partitioned into these three types. The non-monotonic extensions of DLs based on circumscription are very expressive, and the complexity of reasoning increases accordingly, up to undecidability (a common issue afecting many non-monotonic logics). The computational complexity of reasoning in expressive circumscribed DLs has been largely classiifed in [ 6, 8 ]. Moreover, [ 9, 10, 8 ] deal with the low-complexity logics ℰ ℒ and DL-Lite; early preliminary results for DL-Lite can be found in [ 13 ].

In this paper, we focus on the DL-Lite family and address three gaps that remain in the above rich set of results. First, we provide decidability and even tractability results for circumscribed knowledge bases with minimized and fixed roles and nonempty TBoxes . Previous decidability results concerned: (i) ℒ with minimized roles but empty TBoxes (reasoning with nonempty TBoxes is undecidable) [ 6 ], and (ii) DL-LiteBℋool and DL-LiteBℱool with fixed roles [ 8 ].

Second, we extend the analysis of reasoning in the DL-Lite family by addressing concept satisfiability, subsumption, and instance checking (with implications on conjunctive query answering). We refine and extend the lower complexity bounds for query answering in DL-Lite provided in [ 9 ], as well as the recent results in [ 10 ], where—unlike our results—lower complexity bounds rely on priorities, and roles can be neither minimized nor fixed. Similarly, the results of [ 7 ] for DL-Lite extended with defeasible inclusions do not overlap with ours. Defeasible inclusions can be encoded in circumscription (by replacing each ⊑ with ⊓ ¬ ⊑ for a minimized fresh concept name ) but this falls beyond DL-Lite and DL-LiteHorn .

Third, we consider pointwise circumscription in the DL-Lite family. Pointwise circumscribed DLs were introduced in [ 14 ], and the complexity of reasoning has been characterized for ℒℐ [ 15 ]. If roles can be minimized or fixed and nesting of quantifiers is disallowed, then reasoning in pointwise circumscribed ℒℐ is decidable in NExp-time. This is notable since, under the same assumptions, reasoning under global circumscription is undecidable already for ℒ [ 6 ]. In pointwise circumscription, the single global minimality check of classical circumscription is replaced by multiple local minimality checks at all domain elements and their immediate neighborhood. The semantics of [ 15 ] is closely related to pointwise circumscription as introduced by Lifschitz for first-order logic [ 16 ], with some important diferences: varying predicates are not allowed to be reconfigured across the model, and the minimization at a single tuple is replaced by multiple minimizations at one domain element and its direct neighborhood.

We perform a two-dimensional analysis considering the generality of circumscription patterns and the expressiveness of the DL language. Our main contributions are summarized as follows: ∘ Under the assumption that no predicate is varying, concept satisfiability remains tractable in DL-Liteℋ under global and pointwise circumscription. Tractability is not preserved in DL-LiteHorn and Σ2-hardness holds for DL-LiteBool . ∘ Reasoning is intractable already in DL-Lite if predicates are allowed to vary. We provide a Σ 2 upper bound for concept satisfiability in DL-Liteℋ under global circumscription and an NP upper bound for DL-Lite under pointwise circumscription, under some syntactic restrictions. ∘

We show that if no restrictions on the circumscription pattern are assumed, concept satisifability is undecidable in DL-LiteBℋool under global circumscription. The undecidability is shown via a reduction from the domino problem, and it builds a KB in which varying roles are subsumed by minimized ones. We note that the latter falls into a fragment where pointwise circumscription is decidable in NExp-time.

2. Preliminaries

We recall some DLs of the DL-Lite family [ 17 ]. We consider countably infinite, pairwise disjoint sets of concept names and of role names. Roles are either a role name ∈ or its inverse − ; if = − is an inverse role, then − denotes . Basic concepts take the form or ∃, with ∈ a concept name and a role. In basic DL-Lite, concept inclusions take the form 1 ⊑ 2 or 1 ⊑ ¬2 with 1 and 2 basic concepts. We consider also the variants DL-LiteHorn and DL-LiteBool . The former allows concept inclusions of the form 1 ⊓ . . . ⊓ ⊑ and 1 ⊓ . . . ⊓ ⊑ ¬ where and are basic concepts, while in the latter we may write concept inclusions ⊑ , where and are arbitrary Boolean combinations of basic concepts built using ⊓, ⊔ and ¬. Let ℒ be one of DL-Lite, DL-LiteHorn or DL-LiteBool . An ℒ TBox is a finite set of ℒ concept inclusions. We extend these three logics with role inclusions of the form ⊑ , where and are roles. An ℒℋ TBox is a finite set of ℒ concept inclusions and role inclusions. An ℒ(ℋ) knowledge base (KB) is a pair consisting of an ABox and an ℒ(ℋ) TBox. The latter is defined as a finite set of assertions of the forms () and (, ), where ∈ , ∈ , and , are individuals from a countably infinite alphabet , disjoint from and . The semantics of these DLs, and in particular the notion of a model are defined as usual; please see [ 17 ]. We write ℐ |= Γ if ℐ is a model of the TBox or KB Γ, and use (Γ) to denote the set of models of Γ.

2.1. Circumscribed DLs

We recall the notion of circumscription for DLs. Following [ 6 ], we denote circumscription patterns as triples = (, , ), where , , and are mutually disjoint sets partitioning the predicates in , respectively standing for minimized, varying, and fixed predicates1. If is a KB and = (, , ) a circumscription pattern such that , and partition the signature of , we say that “ is circumscribed with the pattern ”, in symbols Circ (). Definition 1. Let = (, , ) be a circumscription pattern, and assume a pair of interpretations ℐ, . We write ℐ ⪯ if the following conditions are satisfied: (i) Δℐ = Δ and ℐ = for all individuals , (ii) ℐ ⊆ for all ∈ , and (iii) ℐ = for all ∈ .

We write ℐ ≺ , if ℐ ⪯ and ℐ ⊂ for some ∈ .

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

Now we recall pointwise circumscription [ 15 ]. We can see that Definition 1 does not restrict in any way how the extension of may difer in ℐ and . It quantifies globally over all subsets of . We call this semantics global circumscription. In pointwise circumscription, we use a more cautious comparability relation ∼ ∙ between interpretations, which may difer only locally on the concepts and roles satisfied by one domain element.

Definition 3. Assume a pair of interpretations ℐ, with Δℐ = Δ and ℐ = , for all ∈ . We write ℐ ∼ ∙ if there exists ∈ Δℐ such that: (i) ℐ ∖ {} = ∖ {} for all concept names , and (ii) ℐ ∩ (Δ × Δ) = ∩ (Δ ×

Δ) for all role names , where Δ = Δℐ ∖ {}. 1We do not assume priorities over the minimized predicates Definition 4. Assume a circumscription pattern and a pair of interpretations ℐ, . We write ℐ ⪯ ∙ , if ℐ ⪯ and ℐ ∼ ∙ . We write ℐ ≺ ∙ , if ℐ ⪯ ∙ and ℐ ⊂ for some ∈ . Definition 5. An interpretation ℐ is a pointwise minimal model of Circ (), in symbols ℐ |=∙ Circ (), if ℐ |= and there is no interpretation s.t. |= and ≺ ∙ ℐ. We use PMM (, ) to denote the set of pointwise minimal models of Circ ().

The reasoning tasks of concept satisfiability, subsumption, and instance checking are adapted to global circumscription and pointwise circumscription. Assume a globally (resp. pointwise) circumscribed knowledge base Circ (): • A concept is satisfiable w.r.t.

PMM (, )) such that ℐ ̸= ∅.

Circ () if there exists ℐ ∈

MM (, ) (resp. • For all concepts and , is subsumed by w.r.t. Circ () if ℐ ⊆ ℐ , for all ℐ ∈ MM (, ) (resp. PMM (, )). In symbols, Circ () |=(∙ ) ⊑ . • Given any individual and any concept , is an instance of w.r.t. Circ () if ℐ ∈ ℐ for all ℐ ∈ MM (, ) (resp. PMM (, )). In symbols, Circ () |=(∙ ) (). In expressive DLs the reasoning tasks above can be interreduced [ 6 ], but in DL-Lite fragments the reductions are trickier. In [ 7 ] the authors provide reductions between reasoning tasks for DL-Liteℋ, but they rely on varying predicates and do not extend to all the settings we consider here.

Example 1. Consider the following simple example: Students normally do not work; Ann is a student. We expect to conclude that Ann does not work. If later it is stated that Ann works, then the previous conclusion should be retracted without deriving any contradiction. This example can be encoded as an instance checking problem in DL-LiteBool with both global and pointwise circumscription, using one abnormality predicate AbStudent:

Student ⊓ ∃hasJob ⊑ AbStudent (a working student is an abnormal student)

Student(Ann) .

If AbStudent is minimized and the other predicates are allowed to vary, then the above knowledge base entails ¬∃hasJob(Ann) (as expected), under both semantics. After adding the assertion ∃hasJob(Ann), the resulting knowledge base is consistent under both semantics and ¬∃hasJob(Ann) is not derivable any longer.

Example 2. Circumscribed DL-Lite allows us to do some reasoning under the closed world assumption. For instance, given the following knowledge base where all predicates are minimized, Student ⊑ Person

Student ⊑ ∃hasStudentCard

Person(Bob)

it can be concluded that ¬Student(Bob) and ¬∃hasStudentCard(Bob), under both semantics.

The next example illustrates the power of circumscription by showing that it may introduce concept unions and functional roles (two features that in general increase complexity). Example 3. Assume the following TBox:

Company_Owner ⊑ Has_Income

Employee ⊑ Has_Income and the pattern = {Has_Income} and = {Company_Owner, Employee}. We can derive that Circ ( ) |= Has_Income ⊑ Company_Owner ⊔ Employee. Moreover, if we add:

Company_Owner(Bob)

Company_Owner ⊑ ∃associated_VAT where associated_VAT ∈ M, one can derive that there is a unique VAT number associated to . Global Circumscription vs Pointwise Circumscription. Pointwise circumscription is a sound approximation of circumscription, as all minimal models are also pointwise minimal. The converse is often true. In fact, we provide a suficient condition in Proposition 1. However, there are cases where they difer, as pointwise minimal models need not be globally minimal. Example 4. Consider the DL-Lite TBox = { ⊑ ∃, ∃− ⊑ } and with the circumscription pattern = (, ∅, ∅) such that = {, }.The interpretation ℐ = {, } with ℐ = {, } and ℐ = {(, ), (, )} is a pointwise minimal model. However, ℐ ̸∈ MM ( , ).

3. Complexity Results

Bonatti et al. [ 6 ] provide an extensive study of the computational complexity of expressive circumscribed DLs. Analogously to the propositional case [ 18, 19, 20 ], the complexity is significantly afected by the choice of the circumscription patterns. We will see that this is also the case for DL-Lite. In the following sections, we study the complexity of reasoning in three DLs in the DL-Lite family [ 17 ] under three diferent forms of circumscription patterns. Definition 6.

Given a circumscription pattern = (, , ), we say that (i) is a basic pattern if = ∅, (ii) is a role-varying pattern if roles are only allowed to vary, i.e. ( ∪ ) ∩ = ∅, (iii) is a general pattern if no restrictions are imposed.

Table 1 summarizes our complexity results. They are stated for concept satisfiability. For basic patterns, we can transfer the lower bounds to the complement of subsumption and instance checking (as concept unsatisfiability easily reduces to subsumption and to instance checking), but without varying predicates, we do not have the converse reductions, thus the P-time upper bound is given only for concept satisfiability. In contrast, both lower and upper bounds in columns 2,3, 5 and 6 apply to the complement of subsumption and instance checking [ 7 ].

Before we delve deeper into the efect of diferent kinds of circumscription patters, we first observe that we can infer some lower bounds from propositional logic. In particular, we can rephrase in our setting some results proved in [ 18 ] for propositional logic under the extended close world assumption (ECWA), and in [19] for circumscribed propositional formulas. This can be done using only concept names, and does not require roles. It is not hard to see that in such a setting global and pointwise circumscription coincide, and we get the following.

Global Circumscription basic varying roles general DL-Lite(ℋ) NL-c ≥ NP and ≤ Σ2 DDLL--LLiittee((BHℋℋooo))rln ≥≥ NΣP2 ≥ ≥ ΣN2Panand d≤ ≤ NΣE2x◇pS ? ≤ P ? ≥ NP undecidable† ≥ Σ2

Pointwise Circumscription basic varying roles general ≥ NP and ≤ NP⋆ ≥ NP ≥ Σ2 ≤ NExp‡ ≤ NExp‡ ≤ NExp‡ • NP-hard for DL-LiteHorn , even with = ∅, • Σ2-hard for DL-LiteBool , even with = ∅.

• NP-hard for DL-Lite if ̸= ∅.

Subsumption and instance checking are hard for the complementary class.

All the NP and Σ2 hardness results in Table 1 follow from this theorem. We devote the rest of the paper to proving the remaining bounds: the membership in NL and P for basic patterns, the membership in NP and Σ2 for varying roles, and the undecidability for general patterns.

3.1. Basic Patterns

In this section, we show that, under the assumption that no predicate is allowed to vary, concept satisfiability is tractable for DL-Liteℋ, under both global and pointwise circumscription. This is remarkable, especially since we allow for roles to be minimized or fixed. For expressive DLs in ℒℐ the latter assumption easily leads to undecidability [ 6 ], while Bonatti et al. [ 7 ] proved that reasoning in ℰ ℒ with defeasible inclusions is undecidable if roles are fixed.

We first observe that the satisfiability of negated concepts is classical in both globally circumscribed and pointwise circumscribed DL-Liteℋ, DL-LiteHℋorn , and DL-LiteBℋool . The latter follows from a result in [ 9 ] (Theorem 5). This does not extend to positive concepts. However, in DL-Liteℋ we can still obtain a tractability result relying on the fact that in a minimal model every object in the extension of a minimized predicate must be justified by an assertion in the ABox or a fixed predicate.

In what follows we assume w.l.o.g. that the given circumscribed KB does not contain inclusions of the form ⊤ ⊑ with ̸∈ . If such inclusions are present, then we can remove them by introducing a fresh concept name , adding the inclusion ⊤ ⊑ and replacing any ⊤ ⊑ ∈ with ⊑ , and extending the circumscription pattern to ′ = (, , ∪ { }); these steps preserve both global and pointwise semantics.

We define the dependency graph of a DL-Liteℋ KB = (, ) as the directed graph () = (, ) where is given by all concept names and role names occurring in , and contains the pairs (, ) for which there exists ∈ such that (1) occurs on the left-hand side of , and (2) occurs on the right-hand side of and is not under negation. Theorem 2. Assume a DL-Liteℋ KB = (, ) and a basic pattern . A concept is satisfiable w.r.t Circ () if has a classical model ℐ with ℐ ̸= ∅ for some predicate such that: (a) there exists a path in () from to if ∈ , and to if is of the form ∃, and (b) is a fixed predicate or occurs in .

Since consistency checking in DL-Liteℋ is complete for NL [ 17 ], and the conditions of Theorem 2 can be checked non-deterministically in logarithmic space, we get: Theorem 3. In DL-Liteℋ concept satisfiability w.r.t. circumscribed KBs where = ∅ is NLcomplete.

The hardness follows from classical reasoning in DL-Liteℋ, which corresponds to circumscribed DL-Liteℋ with all predicates fixed. Under pointwise circumscription, the (if) direction of Theorem 2 holds too, but the (only if) may fail. Recall Example 4. Given the dependency graph of and the concept , one can easily observe that neither (a) nor (b) in Theorem 2 is satisfied. Intuitively, is self-supported, using a cycle involving in the dependency graph of . A characterization very similar to Theorem 2 for pointwise circumscription can be achieved by accommodating such cycles. To do this, we use a more sophisticated dependency graph. Definition 7 (Dependency graph revisited). (Re)define the dependency graph () = (, ) of a DL-Liteℋ KB = (, ) as follows. The set of vertices is the least set containing: • all positive concepts such that for some , either ( ⊑ ) ∈ or ( ⊑ ) ∈ ; • all the concepts such that for some () ∈ • all the concept ∃ and ∃ − such that for some , , (, ) ∈ .

• all nominals {} such that occurs in .

The set of edges , labelled with the symbols in {, }, is the least set containing: • all (, , ) such that there exists ( ⊑ ) ∈ ; • all ({}, , ) such that () ∈ ; • all ({}, , ∃) such that for some , (, ) ∈ ; • all ({}, , ∃− ) such that for some , (, ) ∈ ; • all (∃, , ∃) and (∃− , , ∃− ) such that for ⊑ ∈ ; • all (∃, , ∃− ) such that for some , ( ⊑ ∃) ∈ .

Edges labelled with are called cross edges, while the rest (labelled by ) are inner edges. Definition 8 (Good paths, Cycles). A path in () is a sequence of edges in : (0, ℓ1, 1)(1, ℓ2, 2) · · · (− 1, ℓ, ) .

We say that is a path from 0 to . If = 0 then the path is called a cycle. A path is good if ℓ = implies ℓ+1 ̸= (1 ≤ ≤ − 1), and a cycle is good if ℓ = implies ℓ( mod )+1 ̸= . Definition 9 (Inner segments). An inner segment of a path = 1 . . . in () (where ∈ , for = 1, . . . , ) is a subpath +1 . . . + of (1 ≤ ≤ + ≤ ) such that for all = , . . . , + , is an inner edge of (). Such an inner segment of is maximal if it is not a strict subpath of any inner segment of . An inner segment . . . + of is satisfiable (w.r.t. ) if there exists ℐ ∈ M () such that ℐ ̸= ∅, with = (, ℓ+1, +1).

This refined notion of dependency graph allows us to distinguish cycles in the interpretation from other cycles in the dependency graph. The notion of good cycles ensures that we only consider cycles that pass over more than one object in the interpretation, i.e., passing at least one cross edge, but excluding consecutive symmetric cross edges. The inner segments correspond to sequences of concept implications that may need to hold at one domain element. Theorem 4. Assume a DL-Liteℋ KB = (, ) and a basic pattern . Under pointwise circumscription, a concept is satisfiable w.r.t Circ () if at least one of the following hold: (a) there exists a path from {} to in () and is satisfiable, (b) there exists ∈ with ∈ , or ∈ if is of the form ∃(− ), such that (1) there exists a path from to in (), and (2) there exists ℐ ∈ () such that ℐ ̸= ∅; (c) there exists a path in to from a good cycle involving at least one cross edge, and such that all the maximal inner segments in in the cycle are satisfiable w.r.t. .

Conditions (a) and (b) together check exactly the same conditions as in Theorem 2 (organized and formulated diferently due to the modified definition of ()). The new condition is (c), which identifies when a concept is satisfiable in a pointwise minimal model but not under global circumscription. Example 4 falls into this category: satisfies condition (c). Checking the conditions of Theorem 4 is tractable, but we leave its precise complexity open. Theorem 5. Concept satisfiability in pointwise circumscribed DL-Lite ℋ with = ∅ is in P.

Theorem 2 and Theorem 4 difer only on condition (c), and thus concept satisfiability coincides when () is acyclic. In fact, both semantics coincide for any reasoning task. Proposition 1. Given a KB = (, ) in DL-Liteℋ and a basic pattern , if () is acyclic then PMM (, ) = MM (, ).

3.2. Role-varying Patterns

In this section, we extend circumscription patterns with varying predicates. In particular, we study the complexity under the assumption that all roles are varying. In [ 6 ] circumscription patterns were restricted in this way to obtain decidability and a NExpNP upper bound in ℒℐ. We obtain upper bounds that are significantly lower: Σ2 for global circumscription in DL-Liteℋ, and NP for pointwise circumscription in plain DL-Lite (under some syntactic restrictions on the axioms). The latter is tight by Theorem 1, and we believe that the former may also be so.

Recall the following result from [7, Theorem 4.4], which allows us to eliminate varying concepts: for each concept name ∈ , we introduce a fresh varying role and each occurrence of in is replaced with ∃.

Theorem 6. If ℒ is a DL supporting unqualified existentials, then reasoning w.r.t. (pointwise) circumscribed KBs in ℒ such that ∩ ̸= ∅ can be reduced to reasoning w.r.t. (pointwise) circumscribed KBs in ℒ such that ⊆ .

We assume w.l.o.g. that all concepts are minimized or fixed, while roles are only varying. We show that circumscribed DL-Liteℋ has the small model property, following the model construction for DL-Liteℋ with defeasible inclusions used in [ 7 ].

Lemma 1. Assume a KB in DL-Liteℋ circumscribed with = (, , ), with ⊆ , and a concept . If there exists ℐ ∈ MM (, ) such that ℐ ̸= ∅, then there exists ∈ MM () such that (i) |Δ | is polynomial in the size of , and (ii) ̸= ∅.

Theorem 7. Concept satisfiability in circumscribed DL-Liteℋ with only varying roles is in Σ2.

Subsumption and instance checking are in Π2.

Proof. Assume a concept 0 and a circumscribed KB Circ () in DL-Liteℋ. From Lemma 1, for checking satisfiability of 0 w.r.t. Circ () if sufices to guess an interpretation whose domain is polynomial in the size of and use an NP oracle to check that it is a model of Circ (). NP upper bound for DL-Lite We provide in the full version of the paper an NP algorithm for concept satisfiability in pointwise circumscribed DL-Lite restricted to axioms of the forms ⊑ (¬) and ⊑ (¬) with concept name and a basic concept. That is, we do not allow existentials on both sides of the same axiom. In classical DL-Lite this assumption can be done w.l.o.g., but in pointwise circumscribed DL-Lite traditional normalization cannot be taken for granted [ 15 ]. We use the mosaic technique. First, we define so-called tile types that intuitively are small model fragments. Similarly to [ 15 ], additionally to the local minimality conditions on the tile types, we use special labelings to verify that minimality is preserved when a full model is assembled from tiles. Then we generate a system of extended inequalities that has one variable for each tile type [21]. The solutions to this system of inequalities are functions assigning to each variable a nonnegative integer number or . The inequalities guarantee that, from each solution , if we take () copies of each tile type we assemble correctly a pointwise minimal model. This is very similar to the technique used for obtaining the NExpTime upper bound in [ 15 ]. The key diference here is that, even if the number of variables is exponential in , the number of inequalities is only polynomial in it. Therefore, one only needs to focus on those solutions where only polynomially many variables are nonzero [22]. This allows us to check that a solution exists in nondeterministic polynomial time in the size of the system [21, 23]. Provided that we can check the minimality of a tile type in polynomial time, which is feasible for DL-Liteℋ [ 18 ], we obtain the desired upper bound.

Theorem 8. Concept satisfiability in pointwise circumscribed DL-Lite is NP-complete if ⊆ and no axiom of the form ∃ ⊑ ∃ is allowed.

We belive that the upper bound above holds for pointwise circumscribed DL-Liteℋ without this restriction on the axioms, but leave it open for future work. 3.3. General Patterns In this section, we impose no restriction on the circumscription patterns: concepts and roles may freely participate in the minimized, fixed, and varying predicates. However, we show that already allowing roles to be minimized leads to undecidability in circumscribed DL-LiteBℋool .

We reduce the domino problem to the complement of instance checking, relying heavily on minimized and varying roles. We simulate the TBox constructed in [ 6 ] (see Lemma 27) for showing the undecidability of circumscribed ℒ with minimized roles. Due to space constraints, we focus on explaining how to simulate the axioms that are not expressible in DL-LiteBℋool , and provide the detailed proof in the full version of the paper.

As usual, the key challenge is to enforce a grid. We use the roles and for the horizontal and vertical successor relations. In [ 6 ] the authors use an axiom ⊤ ⊑ ⊔ (∃.∃. ⊓ ∃.∃.¬) to state that a domain element is either in or it does not participate in a correct cell of the grid. We can simulate qualified existentials using auxiliary roles in the usual way. ⊤ ⊑ ⊔ (ℎ ⊓ ℎ)

ℎ ⊑ ∃′ ∃′− ⊑ ℎ′

ℎ′ ⊑ ∃ ′′ ∃ ′′− ⊑

ℎ ⊑ ∃ ′ ∃ ′− ⊑ ′

′ ⊑ ∃′′ ∃′′− ⊑ ¬ ′ ⊑ ′′ ⊑ ′ ⊑ ′′ ⊑ where , and are minimized, while , ℎ, ℎ, ℎ′ , ′ , ′, ′′, ′ and ′′ are varying.

The key challenge now is to propagate a varying ‘error’ concept when an element does not participate in a correct cell of the grid. This is achieved in [ 6 ] with the following ℒ axioms: ¬ ⊑ ⊑ ∀. ⊑ ∀. ∃. ⊑ ∃. ⊑ We instead simulate the following weaker axioms ¬ ⊑ ⊑ ∃. ⊑ ∃. ¬ ⊑ ∃.¬ ¬ ⊑ ∃.¬ using the following set of axioms, and letting all the fresh roles vary: ¬ ⊑

⊑ ∃ℎ ⊓ ∃ ∃ℎ− ⊑ ∃− ⊑ ℎ ⊑ ⊑ ¬ ⊑ ∃¯ ⊓ ∃

¯ ∃¯− ⊑ ¬ ∃¯ − ⊑ ¬ ¯ ⊑ ¯ ⊑ Using the fact that all the varying roles introduced above are subroles of or , and that and are minimized, we can show that, in a minimal model the following claim holds. Claim 1. The roles and are functional at every domain element such that ∈ ¬ℐ .

This allows us to obtain a grid and to lift the undecidability in [ 6 ] to DL-LiteBℋool . Theorem 9. Concept satisfiability in circumscribed DL-Lite Bℋool is undecidable.

We underline that the reduction does not carry over to pointwise circumscribed DL-LiteBℋool as it heavily relies on the fact that in the absence of a proper cell the varying concept is propagated over possibly infinitely many domain elements.

Observe that the TBox above is such that each varying role is subsumed by a minimized one. Under the same assumption, we get a decidability result for pointwise circumscription: Theorem 10. Concept satisfiability in pointwise circumscribed DL-LiteBℋool is in NExp-time under the assumption that varying roles are subsumed by minimized or fixed ones.

The result above follows from the more general result for pointwise circumscribed ℒℐ with no nested quantifiers [ 15 ], extended with the assumption that varying roles are subsumed by minimized ones. With the latter assumption, the mosaic technique used in [ 15 ] can be tuned to accommodate varying roles. (Intuitively, this relies on the fact that varying roles cannot be used for generating new connections).

4. Conclusion

In this paper, we have established several new results for circumscribed logics of the DLLite family. Remarkably, we have established decidability with minimized and fixed roles and nonempty TBoxes, which had only been considered recently in [ 15 ] for more expressive logics under pointwise circumscription, and with significantly higher complexity bounds. Several questions remain for further investigation. For instance, the precise complexity of subsumption for DL-Liteℋ with basic patterns is not yet determined, and we believe that it may be harder than concept satisfiability. For the other patterns with variable predicates we already have NP-hardness results that carry over to subsumption, but we lack matching upper bounds. The lower bounds for role-varying patterns for DL-LiteHorn and DL-LiteBool are inherited from the ifrst column of Table 1, so it is not unlikely that they will not be tight. Table 1 shows that we do not know much about DL-Lite and general patterns under global circumscription. These settings could very well be undecidable, but it is far from obvious how to prove it.

Reducing the complexity of classical circumscription was a key motivation for its pointwise variant, but it seems that it does not always lead to better complexity in the DL-Lite family. It does seem to make things more manageable for DL-Liteℋ and varying roles, where we think that global circumscription is likely to be hard for the second level of the polynomial hierarchy. We want to understand what happens in this case to DL-LiteHorn and DL-LiteBool . Interestingly, for basic patterns in DL-Liteℋ, pointwise circumscription seems to make things more challenging, and may even cause higher complexity.

In this work, we disallowed role disjointness axioms, usually allowed in classical DL-Lite: the latter afects the complexity under circumscription with priorities [ 10 ]. It is open whether this happens also in our settings. We plan to extend circumscription patterns by allowing priorities over minimized predicates, a key ingredient for defeasible DLs. Under the latter assumptions, there are no results for pointwise circumscribed DLs, while for global circumscription some very recent results can be found in [ 10 ]. The data complexity of circumscribed DL-Lite family is also a future research direction worth investigating. Lastly, another interesting direction is to look at ℰ ℒ and extensions, especially under pointwise circumscription.

Acknowledgments

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) project P30873. circumscription, Journal of Computer and System Sciences 48 (1994) 255–310. [19] T. Eiter, G. Gottlob, Propositional circumscription and extended closed-world reasoning are Π2-complete, Theoretical Computer Science 114 (1993) 231–245. doi:https://doi. org/10.1016/0304-3975(93)90073-3. [20] G. Nordh, A trichotomy in the complexity of propositional circumscription, in: F. Baader, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 257–269. [21] 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. [22] I. Pratt-Hartmann, On the computational complexity of the numerically definite syllogistic and related logics, The Bulletin of Symbolic Logic 14 (2008) 1–28. URL: http://www.jstor. org/stable/40039608. [23] C. Lutz, U. Sattler, L. Tendera, The complexity of finite model reasoning in description logics, Inf. Comput. 199 (2005) 132–171.

References

[1] G. Casini , U. Straccia, T. Meyer, A polynomial time subsumption algorithm for nominal safe ℰ ℒ⊥ under rational closure , Information Sciences 501 ( 2019 ) 588 - 620 . URL: https: //www.sciencedirect.com/science/article/pii/S0020025518307436. doi:https://doi.org/ 10.1016/j.ins. 2018 . 09 .037.

[2] F. Donini , M. Lenzerini , D. Nardi , W. Nutt , A. Schaerf , An epistemic operator 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 .

[3] K. Britz , G. Casini, T. Meyer, K. Moodley, U. Sattler , I. Varzinczak , Principles of KLM-style defeasible description logics , ACM Trans. Comput. Log . 22 ( 2021 ) 1: 1 - 1 : 46 .

[4] 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 .

[5] L. Giordano , V. Gliozzi , A. Lieto , N. Olivetti , G. L. Pozzato , Reasoning about typicality and probabilities in preferential description logics , in: Applications and Practices in Ontology Design, Extraction, and Reasoning , volume 49 of Studies on the Semantic Web , IOS Press, 2020 , pp. 145 - 161 .

[6] P. A. Bonatti , C. Lutz , F. Wolter , The complexity of circumscription in DLs , J. Artif. Intell. Res . 35 ( 2009 ) 717 - 773 .

[7] P. A. Bonatti , M. Faella , L. Sauro, Defeasible inclusions in low-complexity DLs , J. Artif. Intell. Res . 42 ( 2011 ) 719 - 764 .

[8] P. A. Bonatti , M. Faella , C. Lutz , L. Sauro , F. Wolter , Decidability of circumscribed description logics revisited , in: Advances in Knowledge Representation, Logic Programming, and Abstract Argumentation , volume 9060 of Lecture Notes in Computer Science, Springer, 2015 , pp. 112 - 124 .

[9] P. A. Bonatti , Query answering in circumscribed OWL2 profiles , Ann. Math. Artif. Intell. 89 ( 2021 ) 1155 - 1173 .

[10] C. Lutz , Q. Manière , R. Nolte , Querying circumscribed description logic knowledge bases , 2023 . arXiv: 2306 . 04546 .

[11] J. McCarthy , Circumscription - A form of non-monotonic reasoning , Artif. Intell . 13 ( 1980 ) 27 - 39 .

[12] V. Lifschitz , Computing circumscription , in: IJCAI, Morgan Kaufmann, 1985 , pp. 121 - 127 .

[13] E. Botoeva , D. Calvanese , Circumscribing dl-lite, IOS Press, 2012 , p. 7 .

[14] F. Di Stefano , M. Ortiz , M. Simkus , Pointwise circumscription in description logics , in: Description Logics , volume 3263 of CEUR Workshop Proceedings, CEUR-WS.org , 2022 .

[15] F. Di Stefano , M. Ortiz , M. Simkus , Description logics with pointwise circumscription, in: IJCAI, ijcai .org, 2023 , pp. 3167 - 3175 .

[16] V. Lifschitz , Pointwise circumscription: Preliminary report , in: AAAI, Morgan Kaufmann, 1986 , pp. 406 - 410 .

[17] A. Artale , D. Calvanese , R. Kontchakov , M. Zakharyaschev, The DL-Lite family and relations , J. Artif. Int. Res . 36 ( 2009 ) 1 - 69 .

[18] M. Cadoli , M. Lenzerini , The complexity of propositional closed world reasoning and