A Datalog Translation for Reasoning on DL-LiteR with Defeasibility

Abstract

Representation of defeasible information is of interest in description logics, as it is related to the need of accommodating exceptional instances in knowledge bases. In this direction, in our previous works we presented a datalog translation for reasoning on (contextualized) OWL RL knowledge bases with a notion of justified exceptions on defeasible axioms. While it covers a relevant fragment of OWL, the resulting reasoning process needs a complex encoding in order to capture reasoning on negative information. In this paper, we consider the case of knowledge bases in DL-LiteR, i.e. the language underlying OWL QL. We provide a definition for DL-LiteR knowledge bases with defeasible axioms and study their properties. The limited form of DL-LiteR axioms allows us to formulate a simpler encoding into datalog (under answer set semantics) with direct rules for reasoning on negative information. The resulting materialization method gives rise to a complete reasoning procedure for instance checking in DL-LiteR with defeasible axioms.

-

Representing defeasible information is a topic of interest in the area of description logics (DLs), as it is related to the need of accommodating the presence of exceptional instances in knowledge bases. This interest led to different proposals for non-monotonic features in DLs based on different notions of defeasibility, e.g. [ 2,4,11,18 ]. In this direction, we presented in [ 6 ] an approach to represent defeasible information in contextualized DL knowledge bases by introducing a notion of justifiable exceptions: general defeasible axioms can be overridden by more specific exceptional instances if their application would provably lead to inconsistency. Reasoning in SROIQ-RL (i.e. OWL RL) knowledge bases is realized by a translation to datalog, which provides a complete materialization calculus [ 19 ] for instance checking and conjunctive query (CQ) answering. While the translation covers the full SROIQ-RL language, it needs a complex encoding to represent reasoning on exceptions. In particular, it relies on the use of proofs by contradiction to ensure completeness in presence of negative disjunctive information.

In this paper, we consider the case of knowledge bases with defeasible axioms in DL-LiteR [ 14 ], which corresponds to the language underlying the OWL QL fragment [ 21 ]. It is indeed interesting to show the applicability of our defeasible reasoning approach to the well-known DL-Lite family: in particular, by adopting DL-LiteR as the base logic we need to take unnamed individuals introduced by existential formulas into account, especially for the justifications of exceptions. Moreover, we show that due to the restricted form of its axioms, the DL-LiteR language allows us to give a less involved datalog encoding in which reasoning on negative information is directly encoded in datalog rules (cf. discussion on “justification safeness” in [ 6 ]). The contributions of this paper can be summarized as follows: – In Section 3 we provide a definition of defeasible DL knowledge base (DKB) with justified models that draws from the definition of Contextualized Knowledge Repositories (CKR) [ 8,9,24 ] with defeasible axioms provided in [ 6 ]. This allows us to concentrate on the defeasible reasoning aspects without considering the aspects related to the representation of context in the CKR framework. – For DKBs based on DL-LiteR, we provide in Section 4 a translation to datalog (under answer set semantics [ 16 ]) that alters the CKR translation in [ 5,6 ] and prove its correctness with respect to instance checking. In particular, the fact that reasoning on negative disjunctive information is not needed allow us to provide a simpler translation (without the use of the involving “test” environments mechanism of [ 6 ]). – In Section 5 we provide complexity results for reasoning problems on DL-LiteRbased DKBs. Deciding satisfiability of such a DKB with respect to justified models is tractable, while inference of an axiom under cautious (i.e., certainty) semantics is co-NP-complete in general.

Further details of the translation are provided in the accompanying Technical Report [ 7 ]. 2

Preliminaries

Description Logics and DL-LiteR language. We assume the common definitions of description logics [ 1 ] and the definition of the logic DL-LiteR [ 14 ]: we summarize in the following the basic definitions used in this work.

A DL vocabulary consists of the mutually disjoint countably infinite sets NC of atomic concepts, NR of atomic roles, and NI of individual constants. Complex concepts are then recursively defined as the smallest sets containing all concepts that can be inductively constructed using the constructors of the considered DL language. A DL-LiteR knowledge base K = hT ; R; Ai consists of: a TBox T containing general concept inclusion (GCI) axioms C v D where C; D are concepts, of the form: C := A j 9R D := A j :C j 9R (1) (2) where A 2 NC and R 2 NR; an RBox R containing role inclusion (RIA) axioms S v R, reflexivity, irreflexivity, inverse and role disjointness axioms, where S; R are roles; and an ABox A composed of assertions of the forms D(a), where D is a rightside concept, R(a; b), with R 2 NR and a; b 2 NI.

A DL interpretation is a pair I = h I ; I i where I is a non-empty set called domain and I is the interpretation function which assigns denotations for language elements: aI 2 I , for a 2 NI; AI I , for A 2 NC; RI I I , for R 2 NR. The interpretation of non-atomic concepts and roles is defined by the evaluation of their description logic operators (see [ 14 ] for DL-LiteR). An interpretation I satisfies an axiom , denoted I j=DL , if it verifies the respective semantic condition, in particular: for = D(a), aI 2 DI ; for = R(a; b), haI ; bI i 2 RI ; for = C v D, CI DI (resp. for RIAs). I is a model of K, denoted I j=DL K, if it satisfies all axioms of K.

Without loss of generality, we adopt the standard name assumption (SNA) in the DL context (see [ 12,15,22 ] for more details). That is, we assume an infinite subset NIS NI of individual constants, called standard names s.t. in every interpretation I we have (i) I = NIIS = fcI j c 2 NIS g; (ii) cI 6= dI , for every distinct c; d 2 NIS . Thus, we may assume that I = NIS and cI = c for each c 2 NIS . The unique name assumption (UNA) corresponds to assuming c 6= d for all constants in NI n NIS resp. occurring in the knowledge base.

We confine here to knowledge bases without reflexivity axioms. The reason is that reflexivity allows one to derive positive properties for any (named and unnamed) individual; this complicates the treatment of defeasible axioms (cf. Discussion section).

Datalog Programs and Answer Sets. We express our rules in datalog with negation

under answer sets semantics. In fact, we use here two kinds of negation3: strong (“classical”) negation : and weak (default) negation not under the interpretation of answer sets semantics [ 16 ]; the latter is in particular needed for representing defeasibility.

A signature is a tuple hC; Pi of a finite set C of constants and a finite set P of predicates. We assume a set V of variables; the elements of C [ V are terms. An atom is of the form p(t1; : : : ; tn) where p 2 P and t1, . . . , tn, are terms. A literal l is either a positive literal p or a negative literal :p, where p is an atom and : is strong negation. Literals of the form p, :p are complementary. We denote with ::l the opposite of literal l, i.e., ::p = :p and :::p = p for an atom p. A (datalog) rule r is an expression: a b1; : : : ; bk; not bk+1; : : : ; not bm: (3) where a; b1; : : : ; bm are literals and not is negation as failure (NAF). We denote with Head (r) the head a of rule r and with Body (r) = fb1; : : : ; bk; not bk+1; : : : ; not bmg the body of r, respectively. A (datalog) program P is a finite set of rules. An atom (rule etc.) is ground, if no variables occur in it. A ground substitution for hC; Pi is any function : V ! C; the ground instance of an atom (rule, etc.) from , denoted , is obtained by replacing in each occurrence of variable v 2 V with (v). A fact H is a ground rule r with empty body. The grounding of a rule r, grnd (r), is the set of all ground instances of r, and the grounding of a program P is grnd (P ) = Sr2P grnd (r).

Given a program P , the (Herbrand) universe UP of P is the set of all constants occurring in P and the (Herbrand) base BP of P is the set of all the ground literals constructable from the predicates in P and the constants in UP . An interpretation I BP is any satisfiable subset of BP (i.e., not containing complementary literals); a literal l is true in I, denoted I j= l, if l 2 I, and l is false in I if ::l is true. Given a rule r 2 grnd (P ), we say that Body (r) is true in I, denoted I j= Body (r), if (i) I j= b for 3 Strong negation can be easily emulated using weak negation. While it does not yield higher expressiveness, it is more convenient for presentation. each literal b 2 Body (r) and (ii) I 6j= b for each literal not b 2 Body (r). A rule r is satisfied in I, denoted I j= r, if either I j= Head (r) or I 6j= Body (r). An interpretation I is a model of P , denoted I j= P , if I j= r for each r 2 grnd (P ); moreover, I is minimal, if I0 6j= P for each subset I0 I.

Given an interpretation I for P , the (Gelfond-Lifschitz) reduct of P w.r.t. I, denoted by GI (P ), is the set of rules obtained from grnd (P ) by (i) removing every rule r such that I j= l for some not l 2 Body (r); and (ii) removing the NAF part from the bodies of the remaining rules. Then I is an answer set of P , if I is a minimal model of GI (P ); the minimal model is unique and exists iff GI (P ) has some model. Moreover, if M is an answer set for P , then M is a minimal model of P . We say that a literal a 2 BP is a consequence of P and write P j= a if every answer set M of P fulfills M j= a. 3

DL Knowledge Base with Justifiable Exceptions

In this paper we concentrate on reasoning on a DL knowledge base enriched with defeasible axioms, whose syntax and interpretation are analogous to [ 6 ]. With respect to the contextual framework presented in [ 6 ], this corresponds to reasoning inside a single local context: while this simplifies presentation of the defeasibility aspects and the resulting reasoning method for the case of DL-LiteR, it can be generalized to the original case of multiple local contexts.

Syntax. Given a DL language L based on a DL vocabulary = NC [ NR [ NI , a defeasible axiom is any expression of the form D( ), where 2 L .

We denote with LD the DL language extending L with the set of defeasible axioms in L . On the base of such language, we provide our definition of knowledge base with defeasible axioms.

Definition 1 (defeasible knowledge base, DKB). A defeasible knowledge base (DKB)

K on a vocabulary is a DL knowledge base over LD .

In the following, we tacitly consider DKBs based on DL-LiteR.

Example 1. We introduce a simple example showing the definition and interpretation of a defeasible existential axiom. In the organization of a university research department, we want to specify that “in general” department members need also to teach at least a course. On the other hand, PhD students, while recognized as department members, are not allowed to hold a course. We can represent this scenario as a DKB Kdept where: Kdept : 8 D(DeptMember v 9hasCourse); Professor v DeptMember ; 9 < PhDStudent v DeptMember ; PhDStudent v :9hasCourse; = : Professor (alice); PhDStudent (bob) ; Intuitively, we want to override the fact that there exists some course assigned to the PhD student bob. On the other hand, for the individual alice no overriding should happen and the defeasible axiom can be applied. 3 Semantics. We can now define a model based interpretation of DKBs, in particular by providing a semantic characterization to defeasible axioms.

Similarly to the case of SROIQ-RL in [ 6 ], we can express DL-LiteR knowledge bases in first-order (FO) logic, where every axiom 2 L is translated into an equivalent FO-sentence 8x: (x) where x contains all free variables of depending on the type of the axiom. The translation, depending on the axiom types, can be defined analogously to the FO-translation presented in [ 6 ]. In the case of existential axioms of the kind = A v 9R, the FO-translation (x) is defined as:

A(x1) ! R(x1; f (x1)) ; that is, we introduce a Skolem function f (x1) which represents new “existential” individuals. Formally, for every right existential axiom 2 L , we define a Skolem function f : NI 7! E where E is a set of new individual constants not appearing in NI. In particular, for a set of individual names N NI, we will write sk(N ) to denote the extension of N with the set of Skolem constants for elements in N .

After this transformation the resulting formulas (x) amount semantically to Horn formulas, since left-side concepts C can be expressed by an existential positive FOformula, and right-side concepts D by a conjunction of Horn clauses. The following property from [6, Section 3.2] is then preserved for DL-LiteR knowledge bases. Lemma 1. For a DL knowledge base K on L , its FO-translation K := V is semantically equivalent to a conjunction of universal Horn clauses. 2K8x (x) With these considerations on the definition of FO-translation, we can now provide our definition of axiom instantiation: Definition 2 (axiom instantiation). Given an axiom 2 L with FO-translation 8x: (x), the instantiation of with a tuple e of individuals in NI , written (e), is the specialization of to e, i.e., (e), depending on the type of .

Note that, since we are assuming standard names, this basically means that we can express instantiations (and exceptions) to any element of the domain (identified by a standard name in NI ). We next introduce clashing assumptions and clashing sets. Definition 3 (clashing assumptions and sets). A clashing assumption is a pair h ; ei such that (e) is an axiom instantiation for an axiom 2 L . A clashing set for a clashing assumption h ; ei is a satisfiable set S that consists of ABox assertions over L and negated ABox assertions of the forms :C(a) and :R(a; b) such that S [f (e)g is unsatisfiable.

A clashing assumption h ; ei represents that (e) is not satisfiable, while a clashing set S provides an assertional “justification” for the assumption of local overriding of on e. We can then extend the notion of DL interpretation with a set of clashing assumptions. Definition 4 (CAS-interpretation). A CAS-interpretation is a structure ICAS = hI; i where I = h I ; I i is a DL interpretation for and is a set of clashing assumptions. By extending the notion of satisfaction with respect to CAS-interpretations, we can disregard the application of defeasible axioms to the exceptional elements in the sets of clashing assumptions. For convenience, we call two DL interpretations I1 and I2 NI-congruent, if cI1 = cI2 holds for every c 2 NI.

Definition 5 (CAS-model). Given a DKB K, a CAS-interpretation ICAS = hI; i is a CAS-model for K (denoted ICAS j= K), if the following holds: (i) for every 2 L in K, I j= ; (ii) for every D( ) 2 K (where 2 L ), with jxj-tuple d of elements in NI such that d 2= fe j h ; ei 2 g, we have I j= (d).

We say that a clashing assumption h ; ei 2 is justified for a CAS model ICAS = hI; i, if some clashing set S = Sh ;ei exists such that, for every CAS-model IC0AS = hI0; i of K that is NI-congruent with ICAS , it holds that I0 j= Sh ;ei. We then consider as DKB models only the CAS-models where all clashing assumptions are justified. Definition 6 (justified CAS model and DKB model). A CAS model ICAS = hI; i of a DKB K is justified, if every h ; ei 2 is justified. An interpretation I is a DKB model of K (in symbols, I j= K), if K has some justified CAS model ICAS = hI; i. Example 2. Reconsidering Kdept in Example 1, a CAS-model providing the intended interpretation of defeasible axioms is ICASdept = hI; dept i where dept = fh ; bobig with = DeptMember v 9hasCourse. The fact that this model is justified is verifiable considering that for the clashing set S = fDeptMember (bob); :9hasCourse(bob)g we have I j= S. On the other hand, note that a similar clashing assumption for alice is not justifiable: it is not possible from the contents of Kdept to derive a clashing set S0 such that S0 [ f (alice)g is unsatisfiable. By Definition 5, this allows to apply to this individual as expected and thus I j= 9hasCourse(alice). 3 DKB-models have interesting properties similar as CKR-models in [ 6 ]. In particular, we mention here that for DKB-model ICAS = hI; i, each clashing assumption h ; ei 2 is over individuals of the knowledge base, cf. [6, Prop. 5, context focus]; this is because in absence of reflexivity, no positive properties (which occur in all clashing sets), can be proven for other elements. Furthermore, the clashing assumptions are non-redundant, i.e., no NI-congruent DKB-model IC0AS = hI0; 0i exists such that 0 , cf. [6, Prop. 6, minimality of justification]. 4

Datalog Translation for DL-LiteR DKB We present a datalog translation for reasoning on DL-LiteR DKBs which refines the translation provided in [ 6 ]. The translation provides a reasoning method for positive instance queries w.r.t. entailment. An important aspect of this translation is that, due to the form of DL-LiteR axioms, no inference on disjunctive negative information is needed for the reasoning on derivations of clashing sets. Thus, differently from [ 6 ], reasoning by contradiction using “test environments” is not needed and we can directly encode negative reasoning as rules on negative literals: with respect to the discussion in [ 6 ], we can say that DL-LiteR thus represents an inherently “justification safe” fragment which then allows us to formulate such a direct datalog encoding. With respect to the interpretation of right-hand side existential axioms, we follow the approach of [ 19 ]: for every axiom of the kind = A v 9R, an auxiliary abstract individual aux is added in the translation to represent the class of all R-successors introduced by .

We introduce a normal form for axioms of DL-LiteR which allows us to simplify the formulation of reasoning rules:4 we can provide rules to transform any DL-LiteR DKB into normal form and show that the rewritten DKB is equivalent to the original. Translation rules overview. We can now present the components of our datalog translation for DL-LiteR based DKBs.5 As in the original formulation in [ 5,6 ], which extended the encoding without defeasibility proposed in [ 9 ] (inspired by the materialization calculus in [ 19 ]), the translation includes sets of input rules (which encode DL axioms and signature in datalog), deduction rules (datalog rules providing instance level inference) and output rules (that encode in terms of a datalog fact the ABox assertion to be proved). The translation is composed by the following sets of rules: DL-LiteR input and output rules: rules in Idlr encode as datalog facts the DL-LiteR axioms and signature of the input DKB. For example, in the case of existential axioms, these are translated as A v 9R 7! fsupEx(A; R; aux )g: note that this rule, in the spirit of [ 19 ], introduces an auxiliary element aux , which intuitively represents the class of all new R-successors generated by the axiom . Similarly, output rules in O encode in datalog the ABox assertions to be proved.

DL-LiteR deduction rules: rules in Pdlr add deduction rules for ABox reasoning. In the case of existential axioms, the rule (pdlr-supex) introduces a new relation to the auxiliary individual as follows: In this translation the reasoning on negative information is directly encoded by “contrapositive” versions of the rules. For example, with respect to previous rule, we have: :instd(x; y)

supEx(y; r; w); const(x); all nrel(x; r): where all nrel(x; r) verifies that :triple(x; r; y) holds for all const(y) by an iteration over all constants.

Defeasible axioms input translations: the set of input rules ID provides the translation of defeasible axioms D( ) in the DKB: in other words, they are used to specify that the axiom need to be considered as defeasible. For example, D(A v 9R) is translated to def supex(A; R; aux ).

Overriding rules: rules for defeasible axioms provide the different conditions for the correct interpretation of defeasibility: the overriding rules define conditions (corresponding to clashing sets) for recognizing an exceptional instance. For example, for axioms of the form D(A v 9R), the translation introduces the rule: ovr(supEx; x; y; r; w)

def supex(y; r; w); instd(x; y); all nrel(x; r): Note that in this version of the calculus, the reasoning on negative information (of the clashing sets) is directly encoded in the deduction rules.

Defeasible application rules: another set of rules in PD defines the defeasible application of such axioms: intuitively, defeasible axioms are applied only to instances that have not been recognized as exceptional. For example, the rule (app-supex) applies a defeasible existential axiom D(A v 9R):

4 The form of DL-LiteR axioms in normal form is shown in [7, Table 1].

5 The full set of rules can be found in the Technical Report [ 7 ].

def supex(y; r; x0); instd(x; y); not ovr(supEx; x; y; r; x0): Translation process. Given a DKB K in DL-LiteR normal form, a program P K(K) that encodes query answering for K is obtained as:

P K(K) = Pdlr [ PD [ Idlr(K) [ ID(K) Moreover, P K(K) is completed with a set of supporting facts about constants: for every literal nom(c), supEx(a; r; c) or def supex(a; r; c) in P K(K), const(c) is added to P K(K). Then, given an arbitrary enumeration c0; : : : ; cn s.t. each const(ci) 2 P K(K), the facts first(c0); last(cn) and next(ci; ci+1) with 0 i < n are added to P K(K). Query answering K j= is then obtained by testing whether the (instance) query, translated to datalog by O( ), is a consequence of P K(K), i.e., whether P K(K) j= O( ) holds.

Correctness. The presented translation procedure provides a sound and complete materialization calculus for instance checking on DL-LiteR DKBs in normal form.

As in [ 6 ], the proof for this result can be verified by establishing a correspondence between minimal justified models of K and answer sets of P K(K).6 Besides the simpler structure of the final program, the proof is simplified by the direct formulation of rules for negative reasoning. Another new aspect of the proof in the case of DL-LiteR resides in the management of existential axioms, since there is the need to define a correspondence between the auxiliary individuals in the translation and the interpretation of existential axioms in the semantics: we follow the approach of Kro¨tzsch in [ 19 ], where, in building the correspondence with justified models, auxiliary constants aux are mapped to the class of Skolem individuals for existential axiom .

As in [ 6 ], in our translation we consider UNA and named models, i.e. interpretations restricted to sk(NK), where NK are the individuals that appear in the input K. Thus we can show the correctness result on Herbrand models, that will be denoted I^( ).

Let ICAS = hI; i be a justified named CAS-model. We define the set of overriding assumptions OVR(ICAS ) = f ovr(p(e)) j h ; ei 2 ; Idlr( ) = p g. Given a CASinterpretation ICAS , we can define a corresponding Herbrand interpretation I(ICAS ) for P K(K): the construction is similar to the one in [ 6 ], by extending it to negative literals and providing an interpretation for existential individuals. The next proposition shows that the least Herbrand model of K can be represented by the answer sets of the program P K(K).

Proposition 1. Let K be a DKB in DL-LiteR normal form. Then: (i). for every (named) justified clashing assumption , the interpretation S = I(I^( )) is an answer set of P K(K); (ii). every answer set S of P K(K) is of the form S = I(I^( )) where is a (named) justified clashing assumption for K.

The correctness result directly follows from Proposition 1.

Theorem 1. Let K be a DKB in DL-LiteR normal form, and let O( ) is defined. Then K j= iff P K(K) j= O( ). 6 A proof sketch for the following results is provided in [ 7 ]. We note that by further normalization of the DKB, the translation can be slimmed at the cost of new symbols. E.g., existential restrictions 9R can be named (A9R 9R) and replaced throughout by A9R; however, we refrain here from further discussion. We first consider the satisfiability problem, i.e., deciding whether a given DL-LiteR DKB has some DKB-model. As it turns out, defeasible axioms do not increase the complexity with respect to satisfiability of DL-LiteR, due to the following property. Let ind(K) denote the set of individuals occurring in K.

Proposition 2. Let K be a DL-LiteR DKB, and let 0 = fh ; ei j D( ) 2 K, e is over ind(K) g be the clashing assumption that makes an exception to every defeasible axiom over the individuals occurring in K. Then K has some DKB-model iff K has some CAS-model ICAS = hI; 0i.

Informally, the only if direction holds because any DKB-model of K is also a CASmodel of K; as justified exceptions are only on ind(K), and making more exceptions does not destroy CAS-modelhood, some CAS-model with clashing assumptions 0 exists. Conversely, if K has some CAS-model of the form ICAS = hI; 0i, a justified CAS-model can be obtained by setting = 0 and trying to remove, one by one, each clashing assumption h ; ei from ; this is possible, if K has some NI-congruent model hI0; n fh ; eigi. After looping through all clashing assumptions in 0, we have that some some NI-congruent model hI0; i exists that is justified.

Thus, DKB-satisfiability testing boils down to CAS-satisfiability checking, which can be done using the datalog encoding described in the previous section. From the particular form of that encoding, we obtain the following result.

Theorem 2. Deciding whether a given DL-LiteR DKB K has some DKB-model is NLogSpace-complete in combined complexity and FO-rewritable in data complexity. To see this, the program P K(K) for K has in each rule at most one literal with an intentional predicate in the body, i.e., a predicate that is defined by proper rules. Thus, we have a linear datalog program with bounded predicate arity, for which derivability of an atom is feasible in nondeterministic logspace, as this can be reduced to a graph reachability problem in logarithmic space. The NLogSpace-hardness is inherited from the combined complexity of KB satisfiability DL-LiteR, which is NLogSpace-complete.

As regards data-complexity, it is well-known that instance checking and similarly satisfiability testing for DL-LiteR are FO-rewritable [ 14 ]; this has been shown by a reformulation algorithm, which informally unfolds the axioms (x) (i.e., performs resolution viewing axioms as clauses), such that deriving an instance A(a) reduces to presence of certain assertions in the ABox. This unfolding can be adorned by typing each argument x 2 x of an axiom to whether it is an individual from the DKB (type i), or an unnamed individual (type u); for example, (x) = A v B yields i(x) and u(x). The typing carries over to unfolded axioms. In unfolding, one omits typed versions of defeasible axioms D( (x)), which w.l.o.g. have no existential restrictions; e.g., for D( (x)) = D(B v C), one omits i(x). In this way, instance derivation (and similarly satisfiability testing) is reduced to presence of certain ABox assertions again.

On the other hand, entailment checking is intractable: while some justified model is constructible in polynomial time, there can be exponentially many clashing assumptions for such models, even under UNA; finding a DKB model that violates an axiom turns out to be difficult.

Theorem 3. Given a DKB K and an axiom , deciding K j= is co-NP-complete; this holds also for data complexity and instance checking, i.e., is of the form A(a) for some assertion A(a).

Proof (Sketch). In order to refute K j= , we can exhibit that a justified CAS-model ICAS = hI; i of K named relative to sk(N ) exists such that I 6j= , with NK N NI n NIS and where N is of small (linear) size and includes fresh individual names such that I violates the instance of for some elements e over sk(N ). We can guess clashing assumptions over N , where each h ; ei 2 has a unique clashing set S (e), and a partial interpretation over N , and check derivability of all S (e) and that the interpretation extends to a model of K relative to sk(N ) in polynomial time. Thus, we overall obtain membership of entailment in co-NP.

The co-NP-hardness can be shown by a reduction from inconsistency-tolerant reasoning from DL-LiteR KBs under AR-semantics [ 20 ]. Given a DL-LiteR KB K = A [ T with ABox A and TBox T , a repair is a maximal subset A0 A such that K0 = A0 [ T is satisfiable; an assertion is AR-entailed by K, if K0 j= for every repair K0 of K. As shown by Lembo et al., deciding AR-entailment is co-NP-hard; this continues to hold under UNA and if all assertions involve only concept resp. role names.

Let K^ = T [ fD( ) j 2 Ag, i.e., all assertions from K are defeasible. As easily seen, the maximal repairs A0 correspond to the justified clashing assumptions by = fh ; ei j (e) 2 A n A0g. Thus, K AR-entails iff K^ j= , proving co-NP-hardness.

To show the result for data complexity, if we do not allow for defeasible assertions, we can adjust the transformation, where we emulate D(A(a)) by an axiom D(A0 v A) and make the assertion A0(a), where A0 is a fresh concept name; similarly D(R(a; b)) is emulated by D(R0 v R) plus R0(a; b), where R0 is a fresh role name. As Lembo et al. proved co-NP-hardness under data-complexity, the claimed result follows. 2 We observe that the co-NP-hardness proof in [ 20 ] used many role restrictions and inverse roles; for combined complexity, co-NP-hardness of entailment in absence of any role names can be derived from results about propositional circumscription in [ 13 ]. In particular, [13, Theorem 16] showed that deciding whether an atom z is a circumscriptive consequence of a positive propositional 2CNF F if all variables except z are minimized (i.e., in circumscription notation CIRC (F ; P; ;; fzg) j= z), is co-NP-hard;7 such an inference can be easily emulated by entailment from a DKB constructed from F and z, where propositional variables are used as concept names.

Indeed, for each clause c = x _ y in F , we add to K an axiom x v :y if z 6= x; y and an axiom x v z (resp. y v z) if z = y (resp. x = z). Furthermore, for each variable 7 The models of CIRC (F ; P; ;; fzg) are all models M of F such that no model M 0 of F exists with M 0 n fzg M n fzg. x 6= z, we add D(x(a)), where a is a fixed individual. This effects that justified DKBmodels of K correspond to the models of CIRC (F ; P; ;; fzg), where the minimality of exceptions in justified DKB-models emulates the minimality of circumscription models; thus, K j= z(a) iff CIRC (F ; P; ;; fzg) j= z. Similarly as above, defeasible assertions could be moved to defeasible axioms D(c v v) with a single assertion c(a).

While this establishes co-NP-hardness of entailment for combined complexity under UNA when roles are absent, the data complexity is tractable; this is because we can consider the axioms for individuals a separately, and if the GCI axioms are fixed only few axioms per individual exist. This is similar if role axioms but no existential restrictions are permitted, as we can concentrate on the pairs a; b and b; a of individuals. The questions remains how much of the latter is possible while staying tractable. 6

Discussion and Conclusion

Related works. The relation of the justified exception approach to nonmonotonic description logics was discussed in [ 6 ], where in particular an in-depth comparison w.r.t. typicality in DLs [ 18 ], normality [ 3 ] and overriding [ 2 ] was given. A distinctive feature of our approach, linked to the interpretation of exception candidates as different clashing assumptions, is the possibility to “reason by cases” inside the alternative justified models (cf. the discussion of the classic Nixon Diamond example [6, Section 7.4]). The introduction of non-monotonic features in the DL-Lite family and, more in general, to low complexity DLs has been the subject of many works, mostly with the goal of preserving the low complexity properties of the base logic in the extension. For example, in [ 3 ] a study of the complexity of reasoning with circumscription in DL-LiteR and E L was presented. Similarly, in [ 17 ] the authors studied the application of their typicality approach to DL-Litec and E L?. A recent work in this direction is [23], where a defeasible version of E L? was obtained by modelling higher typicality by extending classical canonical models in E L? with multiple representatives of concepts and individuals. Summary and future directions. In this paper, we applied the justified exception approach from [ 6 ] to reason on DL-LiteR knowledge bases with defeasible axioms. We have shown that the limited language of DL-LiteR allows us to formulate a direct datalog translation to reason on derivations for negative information in instance checking.

The form of DL-LiteR axioms enables us to concentrate on exceptions in absence of reflexivity over the individuals known from the KB: however, we are interested in studying the case of languages allowing exceptions on unnamed individuals (generated by existential axioms) by providing them with a suitable semantic characterization. In particular, if reflexivity axioms are allowed, positive properties are provable for unnamed individuals (i.e., standard names). To account for this, multiple auxiliary elements aux may be necessary to enable different exceptions for unnamed individuals reached from different individuals; this remains for further investigation.

Moreover, we plan to apply the current results on DL-LiteR in the framework of Contextualized Knowledge Repositories with hierarchies as in [ 10 ]. 22. Motik, B., Rosati, R.: Reconciling description logics and rules. J. ACM 57(5), 30:1–30:62 (2010), https://doi.org/10.1145/1754399.1754403 23. Pensel, M., Turhan, A.: Reasoning in the defeasible description logic E L? - computing standard inferences under rational and relevant semantics. Int. J. Approx. Reasoning 103, 28–70 (2018) 24. Serafini, L., Homola, M.: Contextualized knowledge repositories for the semantic web. J. of Web Semantics 12, 64–87 (2012)

References

1. Baader , F. , Calvanese , D. , McGuinness , D. , Nardi , D. , Patel-Schneider , P . (eds.): The Description Logic Handbook . Cambridge University Press ( 2003 )

2. Bonatti , P.A. , Faella , M. , Petrova , I. , Sauro , L.: A new semantics for overriding in description logics . Artif. Intell . 222 , 1 - 48 ( 2015 )

3. Bonatti , P.A. , Faella , M. , Sauro , L. : Defeasible Inclusions in Low-Complexity DLs . J. Artificial Intelligence Research 42 , 719 - 764 ( 2011 )

4. Bonatti , P.A. , Lutz , C. , Wolter , F. : Description logics with circumscription . In: 10th International Conference on Principles of Knowledge Representation and Reasoning (KR 2006 ). pp. 400 - 410 . AAAI Press ( 2006 )

5. Bozzato , L. , Eiter , T. , Serafini , L. : Contextualized knowledge repositories with justifiable exceptions . In: DL2014. CEUR-WP , vol. 1193 , pp. 112 - 123 . CEUR-WS.org ( 2014 )

6. Bozzato , L. , Eiter , T. , Serafini , L. : Enhancing context knowledge repositories with justifiable exceptions . Artif. Intell . 257 , 72 - 126 ( 2018 )

7. Bozzato , L. , Eiter , T. , Serafini , L. : A Note on Reasoning on DL-LiteR with Defeasibility . CoRR abs/ 1905 .09221 ( 2019 ), http://arxiv.org/abs/ 1905 .09221

8. Bozzato , L. , Homola , M. , Serafini , L. : Towards more effective tableaux reasoning for CKR . In: DL2012. CEUR-WP , vol. 846 , pp. 114 - 124 . CEUR-WS.org ( 2012 )

9. Bozzato , L. , Serafini , L. : Materialization Calculus for Contexts in the Semantic Web . In: DL2013. CEUR-WP , vol. 1014 , pp. 552 - 572 . CEUR-WS.org ( 2013 )

10. Bozzato , L. , Serafini , L. , Eiter , T. : Reasoning with justifiable exceptions in contextual hierarchies . In: 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018 ). pp. 329 - 338 . AAAI Press ( 2018 )

11. Britz , K. , Varzinczak , I.J. : Introducing role defeasibility in description logics . In: Michael, L. , Kakas , A.C. (eds.) JELIA 2016 . LNCS , vol. 10021 , pp. 174 - 189 ( 2016 )

12. de Bruijn, J., Eiter , T. , Tompits , H.: Embedding approaches to combining rules and ontologies into autoepistemic logic . In: 11th International Conference on Principles of Knowledge Representation and Reasoning (KR 2008 ). pp. 485 - 495 . AAAI Press ( 2008 )

13. Cadoli , M. , Lenzerini , M.: The complexity of propositional closed world reasoning and circumscription . J. Comput. Syst. Sci . 48 ( 2 ), 255 - 310 ( 1994 )

14. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Rosati , R. : Tractable reasoning and efficient query answering in description logics: The DL-Lite family . J. Automated Reasoning 39 ( 3 ), 385 - 429 ( 2007 )

15. Eiter , T. , Ianni , G. , Lukasiewicz , T. , Schindlauer , R. , Tompits , H.: Combining answer set programming with description logics for the semantic web . Artif. Intell . 172 ( 12 - 13 ), 1495 - 1539 ( 2008 )

16. Gelfond , M. , Lifschitz , V. : Classical Negation in Logic Programs and Disjunctive Databases . New Generation Computing 9 , 365 - 385 ( 1991 )

17. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.L. : Reasoning about Typicality in Low Complexity DLs: The Logics E L?Tmin and DL-LitecTmin . In: Walsh, T . (ed.) IJCAI 2011 . pp. 894 - 899 . IJCAI/AAAI ( 2011 )

18. Giordano , L. , Gliozzi , V. , Olivetti , N. , Pozzato , G.L.: A non-monotonic description logic for reasoning about typicality . Artif. Intell . 195 , 165 - 202 ( 2013 )

19. Kro¨tzsch, M.: Efficient inferencing for OWL EL . In: Janhunen, T. , Niemela¨, I. (eds.) JELIA 2010 . LNCS , vol. 6341 , pp. 234 - 246 . Springer ( 2010 )

20. Lembo , D. , Lenzerini , M. , Rosati , R. , Ruzzi , M. , Savo , D.F. : Inconsistency-tolerant semantics for description logics . In: RR2010. LNCS , vol. 6333 , pp. 103 - 117 . Springer ( 2010 )

21. Motik , B. , Fokoue , A. , Horrocks , I. , Wu , Z. , Lutz , C. , Grau , B.C. : OWL 2 Web Ontology Language Profiles . W3C recommendation, W3C (Oct 2009 ), http://www.w3.org/TR/ 2009/REC-owl2 - profiles-20091027/