1803.08885

## Defeasible Reasoning in SROEL : from Rational Entailment to Rational Closure Laura Giordano and Daniele Theseider Dupr´ e DISIT - Universit` a del Piemonte Orientale, Alessandria, Italy laura.giordano@uniupo.it, dtd@di.unipmn.it Abstract. In this work we study a rational extension SROEL ( /intersectionsq , × ) R T of the low complexity description logic SROEL ( /intersectionsq , × ) , which underlies the OWL EL ontology language. The extension involves a typicality operator T , whose semantics is based on Lehmann and Magidor's ranked models and allows for the definition of defeasible inclusions. We consider both rational entailment and minimal entailment. We show that deciding instance checking under minimal entailment is in general Π P 2 -hard, while, under rational entailment, instance checking can be computed in polynomial time. We develop a Datalog calculus for instance checking under rational entailment and exploit it, with stratified negation, for computing the rational closure of simple KBs in polynomial time. ## 1 Introduction The need for extending Description Logics (DLs) with nonmonotonic features has led, in the last decade, to the development of several extensions of DLs, obtained by combining them with the most well-known formalisms for nonmonotonic reasoning [2,49,3,18,27,22,38,12,8,14,47,7,39,13,31,6,32] to deal with defeasible reasoning and inheritance, to allow for prototypical properties of concepts and to combine DLs with nonmonotonic rule-based languages under the answer set semantics [22], the wellfounded semantics [21], the MKNF semantics [47,39], as well as in Datalog +/- [37]. Systems integrating Answer Set Programming (ASP) [24,23] and DLs have been developed [50]. In this paper we study a rational extension of the logic SROEL ( /intersectionsq , × ) , introduced by Kr¨ otzsch [41]. It is a low-complexity DL of the EL family [1] that includes local reflexivity, role conjunction and concept products and is at the basis of OWL 2 EL. The rational extension of SROEL ( /intersectionsq , × ) is based on Kraus, Lehmann and Magidor (KLM) preferential semantics [40], and, specifically, on ranked models [43]. We call the logic SROEL ( /intersectionsq , × ) R T and we define notions of rational and minimal entailment for it. Also, we develop a Datalog calculus for instance checking and subsumption under rational entailment and exploit it to construct the rational closure of a knowledge base using stratified negation. The semantics of ranked interpretations for DLs was first studied in [12], where a rational extension of ALC is developed allowing for defeasible concept inclusions of the form C /squareimage D . In this work, following [28,32], we extend the language of SROEL ( /intersectionsq , × ) ˜ with typicality concepts of the form T ( C ) , whose instances are intended to be the typical C elements. Typicality concepts can be used to express defeasible inclusions of the form T ( C ) /subsetsqequal D ('the typical C elements are D '). Here, however, as in [10,26], we allow for typicality concepts to freely occur in concept inclusions. In this respect, the language with typicality that we consider is more general than the language in [32], where T may only occur on the left hand side of inclusions as well as in assertions. For this language, we define a Datalog translation for SROEL ( /intersectionsq , × ) R T which builds on the materialization calculus in [41], and, for reasoning about typicality, exploits the properties of ranked models, by suitably encoding the typicality operator and its properties. We show that instance checking for SROEL ( /intersectionsq , × ) R T can be computed in polynomial time under the rational entailment. Following the approach developed in [41] for SROEL ( /intersectionsq , × ) , the materialization calculus is used to define a Datalog calculus for subsumption in SROEL ( /intersectionsq , × ) R T . The rational closure of a knowledge base has been introduced by Lehmann and Magidor [43] to allow for stronger inferences with respect to preferential and rational entailment, and several constructions of rational closure have been proposed for ALC [14,16,13,32,46]. Such constructions are defined for knowledge bases containing strict or defeasible inclusions and, for the construction in [32], which allows for defeasible inclusions of the form T ( C ) /subsetsqequal D (where C and D are ALC concepts), minimal canonical ranked models have been shown to provide a semantic characterization of rational closure for ALC , thus generalizing to DLs the canonical model result in [43]. Based on the same construction introduced in [32] for ALC , in this paper we use the Datalog calculus for SROEL ( /intersectionsq , × ) R T plus stratified negation to compute in polynomial time the Rational Closure for simple SROEL ( /intersectionsq , × ) R T KBs, where the typicality operator only occurs on the left hand side of inclusions. However, not for all simple knowledge bases the rational closure is consistent. Indeed, the minimal canonical model semantics does not provide a general semantic characterization of the rational closure for SROEL ( /intersectionsq , × ) with typicality, as a KB may have alternative minimal canonical models with incompatible rankings, or no canonical model at all. In particular, we show that instance checking in SROEL ( /intersectionsq , × ) R T under the minimal canonical model semantics is Π p 2 -hard. We observe that, even in cases when the KB has no minimal canonical model, the rational closure, when consistent, may still provide meaningful consequences. A preliminary version of some results in the paper appeared in [34], and a version including the calculus for rational entailment in [35]. In this paper we also exploit the calculus for computing the rational closure of a (simple) SROEL ( /intersectionsq , × ) R T KB in polynomial time. Furthermore, we provide a Π P 2 lower bound on the complexity of instance checking under the minimal canonical model semantics, thus strengthening the result in [34,35]. ## 2 A rational extension of SROEL ( /intersectionsq , × ) In this section we recall the logic SROEL ( /intersectionsq , × ) R T introduced in [33,35] extending the notion of concept in SROEL ( /intersectionsq , × ) by adding typicality concepts. We refer to [41] for a detailed description of the syntax and semantics of SROEL ( /intersectionsq , × ) . We let N C be a set of concept names, N R a set of role names and N I a set of individual names. A concept in SROEL ( /intersectionsq , × ) is defined as follows: <!-- formula-not-decoded --> where A ∈ N C and R,S ∈ N R . We introduce a notion of extended concept C E as follows: <!-- formula-not-decoded --> where C is a SROEL ( /intersectionsq , × ) concept. Hence, any concept of SROEL ( /intersectionsq , × ) is also an extended concept; a typicality concept T ( C ) is an extended concept and can occur in conjunctions and existential restrictions, but it cannot be nested. A KB is a triple ( TBox , RBox , ABox ) . TBox contains a finite set of general concept inclusions (GCI) C /subsetsqequal D , where C and D are extended concepts; RBox (as in [41]) contains a finite set of role inclusions of the form S /subsetsqequal T , generalized role inclusions of the form R ◦ S /subsetsqequal T , role conjunction axioms R /intersectionsq S /subsetsqequal T and concept product axioms C × D /subsetsqequal T and R /subsetsqequal C × D , where C and D are extended concepts, and R,S,T are role names in N R . ABox contains individual assertions of the form C ( a ) and R ( a, b ) , where a, b ∈ N I , R ∈ N R and C is an extended concept. Restrictions are imposed on the use of roles as in [41] (and, in particular, all the roles occurring in Self concepts and in role conjunctions must be simple roles , roughly speaking, roles which do not include the composition of other roles). We define a semantics for SROEL ( /intersectionsq , × ) R T based on ranked models [43]. As done in [32] for ALC , we define the semantics of SROEL ( /intersectionsq , × ) R T by adding to SROEL ( /intersectionsq , × ) interpretations [41] a preference relation < on the domain, which is intended to compare the 'typicality' of domain elements. The typical instances of a concept C , i.e., the instances of T ( C ) , are the instances of C that are minimal with respect to < . The properties of the < relation are defined in agreement with the properties of the preference relation in Lehmann and Magidor's ranked models [43]. A semantics for DLs with defeasible inclusions based on ranked models was first proposed in [12]. Definition 1. A SROEL ( /intersectionsq , × ) R T interpretation M is any structure 〈 ∆,<, · I 〉 where: - -∆ is a domain; · I is an interpretation function that maps each concept name A ∈ N C to a set A I ⊆ ∆ , each role name R ∈ N R to a binary relation R I ⊆ ∆ × ∆ , and each individual name a ∈ N I to an element a I ∈ ∆ ; the extension of · I to complex concepts is defined as usual: - -< is an irreflexive, transitive, well-founded and modular relation over ∆ ; - -the interpretation of concept T ( C ) is defined as: ( T ( C )) I = Min < ( C I ) , where Min < ( S ) = { u : u ∈ S and /notexistential z ∈ S s.t. z < u } . ``` ``` Furthermore, an irreflexive and transitive relation < is well-founded if, for all S ⊆ ∆ , for all x ∈ S , either x ∈ Min < ( S ) or ∃ y ∈ Min < ( S ) such that y < x . It is modular if, for all x, y, z ∈ ∆ , x < y implies x < z or z < y . The well-foundedness condition guarantees that if, for a non-extended concept C , there is a C element in M , then there is a minimal C element in M (i.e., C I = ∅ implies ( T ( C )) I = ∅ ). /negationslash /negationslash In the following, we will refer to SROEL ( /intersectionsq , × ) R T interpretations as ranked interpretations . Indeed, as in [43], modularity in preferential models can be equivalently defined by postulating the existence of a rank function k M : ∆ ↦-→ Ω , where Ω is a totally ordered set. The preference relation < can be defined from k M as follows: x < y if and only if k M ( x ) < k M ( y ) . Hence, in the following, we will assume that a rank function k M is always associated with any model M . We also define the rank k M ( C ) of a concept C in the model M as k M ( C ) = min { k M ( x ) | x ∈ C I } (if C I = ∅ , then C has no rank and we write k M ( C ) = ∞ ). The semantics of the typicality operator defined above is the same as the one in [32] for ALC + T R . Similarly to other concept constructors, the typicality operator can be used in TBox and ABox with different restrictions, depending on the description logic. In [32], T ( C ) can only occur on the left-hand side of concept inclusions (namely, in typicality inclusions of the form T ( C ) /subsetsqequal D ). Here, we call simple KBs the ones which respect this restriction, but, as in [10,26], we also consider the general case with no restrictions on the occurrences of typicality concepts T ( C ) in concept inclusions and assertions. Instead, as in SROEL ( /intersectionsq , × ) , we do not allow negation, union and universal restriction which are allowed in ALC . Given an interpretation M , the notions of satisfiability and entailment are defined as usual: ## Definition 2 (Satisfiability and rational entailment). An interpretation M = 〈 ∆,< - , · I 〉 satisfies: - a concept inclusion C /subsetsqequal D if C I ⊆ D I ; - a role inclusion S /subsetsqequal T if S I ⊆ T I ; - a generalized role inclusion R ◦ S /subsetsqequal T if R I ◦ S I ⊆ T I - a role conjunction axiom R /intersectionsq S /subsetsqequal T if R I ∩ S I ⊆ T I ; - a concept product axiom C × D /subsetsqequal T if C I × D I ⊆ T I ; - a concept product axiom R /subsetsqequal C × D if R I ⊆ C I × D I ; - an assertion C ( a ) if a I ∈ C I ; - an assertion R ( a, b ) if ( a I , b I ) ∈ R I . Given a KB K = ( TBox , RBox , ABox ) , an interpretation M = 〈 ∆,<, · I 〉 satisfies TBox (resp., RBox , ABox ) if M satisfies all axioms in TBox (resp., RBox , ABox ), and we write M| = TBox (resp., RBox , ABox ). An interpretation M = 〈 ∆,<, · I 〉 is a model of K (and we write M| = K ) if M satisfies all the axioms in TBox , RBox and ABox . Let a query F be either a concept inclusion C /subsetsqequal D (where C and D are extended concepts) or an individual assertion. F is rationally entailed by K , written K | = sroelrt F , if for all models M = 〈 ∆,<, · I 〉 of K , M satisfies F . In particular, the instance checking problem (under rational entailment) is the problem of deciding whether an assertion ( C ( a ) , T ( C )( a ) or R ( a, b ) ) is rationally entailed by K . Given the correspondence of typicality inclusions with conditional assertions C | ∼ D , it can be easily seen that each ranked interpretation M satisfies the following semantic conditions, which are related to Lehmann and Magidor's postulates of rational consequence relation [43] reformulated in terms of typicality: ``` ``` It is easy to show that these semantic properties (where the interpretation of A /unionsq B , which is not in the language, is the usual one) hold in all the ranked models. A similar formulation of the semantic properties in terms of defeasible inclusions has been previously provided by Britz et al. in [12], for the ranked semantics and a proof can be found in [46]. Another reformulation of the properties in terms of a selection function semantics was given in [28] for the preferential semantics and in [32] for the rational semantics. In particular, observe that property ( S -RM ) can be reformulated as: ``` ``` /negationslash and, in this form, it is a rephrasing of property ( f T -R ) , in the semantics with selection function of the operator T studied in [32] (Appendix A) for ALC + T R . This property has a syntactic counterpart in SROEL ( /intersectionsq , × ) in the axiom ∃ U. ( T ( A ) /intersectionsq B ) /intersectionsq T ( A /intersectionsq B ) /subsetsqequal T ( A ) , where U is the universal role ( /latticetop ×/latticetop /subsetsqequal U ), which holds in all the ranked models. Observe that this axiom, as well as the property ( S -RM ) , is weaker than the Lehmann and Magidor's postulate ( RM ) in [43], which would rather be reformulated, for a knowledge base K , as: ``` ``` and does not hold in SROEL ( /intersectionsq , × ) R T (while it will hold under minimal entailment). Consider the following example of knowledge base, stating that: typical Italians have black hair; typical students are young; they hate math, unless they are nerd (in which case they love math); all Mary's friends are typical students. We also have the assertions stating that Mary is a student, that Mario is an Italian student, and is a friend of Mary, Luigi is a typical Italian student, Paul is a typical young student, and Tom is a typical nerd student. ## Example 1. TBox : - ( a ) T ( Italian ) /subsetsqequal ∃ hasHair . { Black } - ( b ) T ( Student ) /subsetsqequal Young - ( c ) T ( Student ) /subsetsqequal MathHater - ( d ) T ( Student /intersectionsq Nerd ) /subsetsqequal MathLover - ( e ) ∃ hasHair . { Black } /intersectionsq ∃ hasHair . { Blond } /subsetsqequal ⊥ - ( f ) MathLover /intersectionsq MathHater /subsetsqequal ⊥ - ( g ) ∃ friendOf . { mary } /subsetsqequal T ( Student ) ABox : Student ( mary ) , friendOf ( mario , mary ) , ( Student /intersectionsq Italian )( mario ) , T ( Student /intersectionsq Italian )( luigi ) , T ( Student /intersectionsq Young )( paul ) , T ( Student /intersectionsq Nerd )( tom ) The fact that concepts T ( C ) can occur anywhere (apart from being nested in a T operator) can be used, e.g., to state that typical working students inherit properties of typical students ( T ( Student /intersectionsq Worker ) /subsetsqequal T ( Student ) ), in a situation in which typical students and typical workers have conflicting properties (e.g., as regards paying taxes). Also, we could state that there are typical students who are Italian: /latticetop /subsetsqequal ∃ U. T ( Student /intersectionsq Italian ) . Standard DL inferences hold for T ( C ) concepts and T ( C ) /subsetsqequal D inclusions. For instance, we can conclude that Mario is a typical student (by (g)) and young (by (b)). However, by the properties of defeasible inclusions, Luigi, who is a typical Italian student, and Paul, who is a typical young student, both inherit the property of typical students of being math haters, respectively, by properties (S-RM) and (S-CM). Instead, as Tom is a typical nerd student, and typical nerd students are math lovers, this specific property of typical nerd students prevails over the less specific property of typical students of hating math. So we can consistently conclude that Tom is a MathLover . A normal form for SROEL ( /intersectionsq , × ) R T knowledge bases can be defined. A KB in SROEL ( /intersectionsq , × ) R T is in normal form if it admits all the axioms of a SROEL ( /intersectionsq , × ) KB in normal form: <!-- formula-not-decoded --> (where A,B,C,D ∈ N C , R,S,T ∈ N R and a, b, c ∈ N I ) and, in addition, it admits axioms of the form: A /subsetsqequal T ( B ) and T ( B ) /subsetsqequal C with A,B,C ∈ N C . Extending the results in [1] and in [41], it is easy to see that, given a SROEL ( /intersectionsq , × ) R T KB, a semantically equivalent KB in normal form (over an extended signature) can be computed in linear time. In essence, for each concept T ( C ) occurring in the KB, we introduce two new concept names, X C and Y C . A new KB is obtained by replacing all the occurrences of T ( C ) with X C in all the inclusions and assertions, and adding the following additional inclusion axioms: <!-- formula-not-decoded --> Then the new KB undergoes the normal form transformation for SROEL ( /intersectionsq , × ) [41]. The resulting KB is linear in the size of the original one. Example 2. Considering the TBox in Example 1, inclusion - ( a ) T ( Italian ) /subsetsqequal ∃ hasHair . { Black } is transformed in the following set of inclusions: - ( a 1 ) X I /subsetsqequal ∃ hasHair . { Black } ( a 2 ) X I /subsetsqequal T ( Italian ) ( a 3 ) T ( Italian ) /subsetsqequal X I Inclusion ( d ) T ( Student /intersectionsq Nerd ) /subsetsqequal MathLover is mapped to the set of inclusions: - ( d 1 ) X SN /subsetsqequal MathLover ( d 2 ) X SN /subsetsqequal T ( Y SN ) ( d 3 ) T ( Y SN ) /subsetsqequal X SN - ( d 4 ) Student /intersectionsq Nerd /subsetsqequal Y SN ( d 5 ) Y SN /subsetsqequal Student /intersectionsq Nerd Then ( a 1 ) is transformed further (the normal form transformation for SROEL ( /intersectionsq , × ) ) into: ( a ′ 1 ) X I /subsetsqequal ∃ hasHair . B , and ( a ′′ 1 ) B /subsetsqequal { Black } , while ( d 5 ) is split in two inclusions. All the other axioms in the TBox, apart from (b) and (c), have to be transformed in normal form. Assertions are also subject to the normal form transformation. For instance, T ( Student /intersectionsq Nerd )( tom ) becomes X SN ( tom ) , where X SN is one of the concept names introduced above. ## 3 Minimal entailment In Example 1, we cannot conclude that all typical young Italians have black hair (and in case Bob is a typical young Italian, he has black hair) using property (S-RM) above, as we do not know whether there is some typical Italian who is also young. To support such a stronger nonmonotonic inference, a minimal model semantics is needed to select those interpretations where individuals are as typical as possible. Among models of a KB, we select the minimal ones according to the following preference relation ≺ over the set of ranked interpretations . An interpretation M = 〈 ∆,<,I 〉 is preferred to M ′ = 〈 ∆ ′ , < ′ , I ′ 〉 ( M≺M ′ ) if: ∆ = ∆ ′ ; C I = C I ′ for all non-extended concepts C ; for all x ∈ ∆ , k M ( x ) ≤ k M ′ ( x ) , and there exists y ∈ ∆ such that k M ( y ) < k M ′ ( y ) . We say that an interpretation M = 〈 ∆,<,I 〉 is a minimal model of K if there is no model M ′ = 〈 ∆ ′ , <, ′ I ′ 〉 of K such that M ′ ≺ M . We can see that in all the minimal models of the KB in Example 1, luigi is an instance of the concept ∃ hasHair . { Black } and the inclusion T ( Young /intersectionsq Italian ) /subsetsqequal ∃ hasHair . { Black } is satisfied, as nothing prevents a Young /intersectionsq Italian individual from having rank 0 . In particular, we consider the notion of minimal canonical model defined in [32] to capture rational closure of an ALC KB extended with typicality. The requirement of a model to be canonical is used to guarantee that models contain enough individuals. Given a KB K and a query F , let S be the set of all the (non-extended) concepts (and subconcepts) occurring in K or F together with their complements ( S is finite). In the following, we assume that all concepts occurring in the query F are included in K . Definition 3 (Canonical models). A model M = 〈 ∆,<,I 〉 of K is canonical if, for each set of SROEL ( /intersectionsq , × ) R T concepts { C 1 , C 2 , . . . , C n } ⊆ S consistent with K (i.e., s.t. K /negationslash| = sroelrt C 1 /intersectionsq C 2 /intersectionsq . . . /intersectionsq C n /subsetsqequal ⊥ ), there exists (at least) a domain element x ∈ ∆ such that x ∈ ( C 1 /intersectionsq C 2 /intersectionsq . . . /intersectionsq C n ) I . Definition 4. M is a minimal canonical model of K if it is a canonical model of K and it is minimal with respect to the preference relation ≺ . Definition 5 (Minimal entailment). Given a query F , F is minimally entailed by K , written K | = c min F if, for all minimal canonical models M of K , M satisfies F . We can show that instance checking in SROEL ( /intersectionsq , × ) R T under minimal entailment is Π P 2 -hard. The proof is based on a reduction of the minimal entailment problem of positive disjunctive logic programs , which has been proved to be a Π P 2 -hard problem by Eiter and Gottlob in [19]. A similar reduction has been used to prove Π P 2 -hardness of entailment for Circumscribed Left Local EL ⊥ knowledge bases in [7], and in [33] to show that instance checking under the T -minimal model semantics (a different semantics) is a Π P 2 -hard problem for SROEL ( /intersectionsq , × ) R T knowledge bases. The reduction in [33] (Appendix B in the 'Supplementary materials') does not work for the minimal canonical model semantics, since the resulting knowledge base may have no canonical model, but a simplification of it does work. Let us recall the minimal entailment problem of positive disjunctive logic programs [19]. Let PV = { p 1 , . . . , p n } be a set of propositional variables. A clause is a formula l 1 ∨ . . . ∨ l h , where each literal l j is either a propositional variable p i or its negation ¬ p i . A positive disjunctive logic program (PDLP) is a set of clauses S = { γ 1 , . . . , γ m } , where each γ j contains at least one positive literal. A truth valuation for S is a set I ⊆ PV , containing the propositional variables which are true. A truth valuation is a model of S if it satisfies all clauses in S . For a literal l , we write S | = min l if and only if every minimal model (with respect to subset inclusion) of S satisfies l . The minimal-entailment problem can be then defined as follows: given a PDLP S and a literal l , determine whether S | = min l . In the following we sketch the reduction of the minimal-entailment problem for a PDLP S to the instance checking problem under minimal entailment, from a knowledge base K constructed from S . We define a KB K = ( TBox , RBox , ABox ) in SROEL ( /intersectionsq , × ) R T as follows. We introduce a concept name P h ∈ N C for each variable p h ∈ PV ( h = 1 , . . . , n ). Also, we introduce in N C an auxiliary concept H , a concept name D S associated with the set of clauses S , and a concept name D j associated with each clause γ j in S ( j = 1 , . . . , m ). We let a ∈ N I be an individual name, and we define K as follows: RBox = ∅ , ABox = { P h ( a ) , h = 1 , . . . , n } ∪ { T ( H )( a ) , D S ( a ) } , and TBox contains the following inclusions (where C j i and C j i are concepts associated with each literal l j i occurring in γ j = l j 1 ∨ . . . ∨ l j k , as defined below): <!-- formula-not-decoded --> <!-- formula-not-decoded --> for each h = 1 , . . . , n , j = 1 , . . . , m , and where C j i and C j i (for i = 1 , . . . , k ) are defined as follows: <!-- formula-not-decoded --> <!-- formula-not-decoded --> where U is the universal role. Let us consider an arbitrary model M = 〈 ∆,<, · I 〉 of K . Observe that, by (1), all the T ( /latticetop ) instances are ¬ H instances. Hence, a I (being a typical H ) must have rank greater than 0, and it will have rank 1 in all minimal canonical models. Inclusions (2) and (3) force the instances of D j to be the union of the instances of C j 1 , . . . , C j k . Inclusions (4) and (5) force the instances of D S to be the intersection of the instances of D 1 , . . . , D m . The minimal canonical models of K satisfying D S ( a ) are intended to correspond to the (propositional) minimal interpretation J satisfying S . Roughly speaking, the concepts P h such that a I ∈ ( T ( P h )) I in M correspond to the variables p h true in the interpretation J satisfying S . In any minimal canonical model of K , either P h has rank 0 (and a is not a typical P h ), or P h has rank 1 (and a is a typical P h ). Also, a minimal model of K in which the ranking of a set of P h 's is 0, is preferred to the models in which the ranking of some of those P h 's is higher (i.e., 1). This captures the subset inclusion minimality in the interpretations of the positive disjunctive logic program S . The assertion D S ( a ) in ABox is required to select only those interpretations satisfying the set S of disjunctions. Observe also that a is an istance of P h for all h (due to the Abox) but it may be a non-typical instance of P h . In any minimal canonical model M of K : either a I ∈ ( T ( P h )) I or a I ∈ ( ∃ U . ( T ( /latticetop ) /intersectionsq T ( P h ))) I . Hence, for a I the two concepts in the definition of C j i are disjoint and complementary, and C j i is actually the concept representing the complement of C j i . Proposition 1. Given a set S of clauses and a literal L , S | = min L if and only if K | = c min C L ( a ) where K is the KB associated with S as above and C L is the concept associated with L , i.e., C L = T ( P h ) if L = p h , and C L = ∃ U. ( T ( /latticetop ) /intersectionsq P h ) if L = ¬ p h . Proof. ( ⇒ ) We prove that if K /negationslash| = c min C L ( a ) then S /negationslash| = min L . Let M = 〈 ∆,< , · I 〉 be a minimal canonical model of K falsifying C L ( a ) . We want to construct a (propositional) interpretation J satisfying S and falsifying L . Let J be the set of all the variables p h such that a is a typical P h element, i.e., J = { p h : a I ∈ T ( P h ) I } . We show that J is a minimal model of S that falsifies L . The fact that J is a model of S can be easily shown from the fact that p h ∈ J iff M| = T ( P h )( a ) , while p h /negationslash∈ J iff M /negationslash| = T ( P h )( a ) i.e., iff M | = ∃ U. ( T ( /latticetop ) /intersectionsq P h )( a ) . In fact when M /negationslash| = T ( P h )( a ) , P h must have rank lower than a , i.e. rank 0 . Hence, a literal l j i is true in J iff C j i ( a ) is satisfied in M and it is false in J if C j i ( a ) is satisfied in M . From the facts that the concepts C j i and C j i are disjoint and complementary for a , that inclusions (2)-(5) are satisfied and that D S ( a ) is satisfied as well, it follows that the interpretation J satisfies all the clauses in S . Consider a clause γ j in S . As D S ( a ) is satisfied in M , D j ( a ) must be satisfied as well, by (5). By (3) it is not the case that ( C j 1 /intersectionsq . . . /intersectionsq C j k )( a ) is satisfied in M . There must be a C j h for h = 1 , . . . , k , such that C j h ( a ) is satisfied in M . Hence, the literal l j h must be satisfied in J . Thus, γ j is satisfied in J . This holds for all the clauses γ j in S . Hence, J satisfies S . In a similar way it can be seen that, as C L ( a ) is falsified in M , then the literal L is falsified in J . The minimality of J can be proved by contradiction. If J were not minimal, there would be a model J ′ of S , with J ′ ⊆ J . First observe that, for any valuation I ⊆ PV we can define a concept C I obtained as the conjunction of the name concepts in the set Γ I = { P h : p k ∈ I } ∪ {¬ P h : p k /negationslash∈ I } and C I is consistent with K . In fact, we can always add to a model of K a new domain element with rank 1 satisfying C I as well as the inclusions (1)-(5) (by properly defining the evaluation of the concepts D j 's and of D S ), to obtain a new model of K . In particular, in a canonical model, for each propositional valuation I ⊆ PV , there must be a domain element which is an instance of C I . For J ′ ⊆ J , let I = J -J ′ . There must be an element z ∈ ∆ of M which is an instance of C I and, furthermore, k M ( z ) ≥ 1 (if not, T ( P h )( a ) would not be satisfiable in M for all p h ∈ I = J -J ′ , contradicting the fact that, by construction of J , for each p h ∈ J , T ( P h )( a ) is satisfiable in M ). We can define a model M ′ such that M ′ ≺ M , by only changing the rank of z in M to 0 . We can easily see that M ′ is still a model of K , a model in which, for all p h ∈ J -J ′ , T ( P h )( a ) is not satisfied, but in which inclusions (1)-(5) and the ABox assertions are still satisfied (given that J ′ is a model of S and that M ′ | = T ( P h )( a ) iff p h ∈ J ′ ). This contradicts the hypothesis that M is minimal. ``` ``` Let J be a (propositional) minimal interpretation satisfying S and falsifying L . We build a minimal canonical model of K falsifying C L ( a ) , as follows. Let M = 〈 ∆,<, · I 〉 be defined as follows (where r = 1 , 2 and h = 1 , . . . , n ): ``` ``` /negationslash Finally, for all y ∈ ∆ such that y = u , for each j = 1 , . . . , m , we let y ∈ D I j iff some literal l j i of γ j is true in J ; and, also, y ∈ D I S iff y is an instance of all D 1 , . . . , D m . It turns out that, for all the variables p h ∈ J , u is an instance of T ( P h ) while, for all the variables p h /negationslash∈ J , v is an instance of T ( P h ) and all domain elements are instances of ∃ U. ( T ( /latticetop ) /intersectionsq P h ) . It is easy to see that M is a model of K , as it satisfies all the assertions and inclusions in K . Also, M is a canonical model of K , as all the non-extended concepts occurring in K have an instance in the model. To see that M falsifies C L ( a ) , we proceed by cases. Consider the case where L = p h and C L = T ( p h ) . In this case, p h /negationslash∈ J and, by construction, a I /negationslash∈ T ( P h ) I , so that M falsifies C L ( a ) . Consider the case when L = ¬ p h and C L = ∃ U. ( T ( /latticetop ) /intersectionsq P h ) . It must be that p h ∈ J and, by construction, a I ∈ T ( P h ) I . As there is no domain element with rank 0 which is an instance of P h , a /negationslash∈ ( ∃ U. ( T ( /latticetop ) /intersectionsq P h )) I . Hence, M falsifies C L ( a ) . The minimality of M among the canonical models of K can be shown by contradiction. Suppose that M is not minimal, then there is a canonical model M ′ = 〈 ∆ ′ , <, · I ′ 〉 of K (with ∆ ′ = ∆ and I ′ = I ) such that M ′ ≺ M . Hence there must be at least one concept C which has rank 1 in M and rank 0 in M ′ . In particular, some concept P h , with h = 1 , . . . , n , must have rank 1 in M and rank 0 in M ′ . In fact, the concept H cannot have rank 0 in any model of K (by inclusion (1)), and the interpretation of all other concepts is determined by the interpretation of the P h 's (given inclusions (2)-(5)). Let { P j 1 , . . . , P j r } be the set of concepts having rank 1 in M and rank 0 in M ′ , while all other concepts P h keep the same rank in M ′ as in M . It is easy to see that, as M ′ is a model of K , it is possible to construct from M ′ a model J ′ of S such that J ′ ⊆ J , thus contradicting the hypothesis that J is a minimal model of S . From the reduction above and the fact that minimal entailment for PDLP is Π P 2 -hard [19], it follows: Theorem 1. Minimal entailment under minimal canonical model semantics is Π P 2 -hard. It is an open issue whether a similar proof can be given also for simple knowledge bases (as defined in section 2). For simple KBs in ALC + T R , it was proved in [32] that all minimal canonical models of the KB assign the same ranks to concepts, namely, the ranks determined by the rational closure construction. This result also holds for the fragment of SROEL ( /intersectionsq , × ) R T included in the language of ALC plus typicality, which however, does not contain nominals, role inclusions, and other constructs of SROEL ( /intersectionsq , × ) . The presence of the new constructs and of role inclusions makes alternative minimal canonical model arise with incomparable rankings for concepts. Even worst, a KB may have no canonical model. This makes the adequacy of the minimal canonical model semantics disputable, and in [33] an alternative T -minimal model semantics has been introduced, which coincides with the minimal canonical model semantics under some conditions. The existence of alternative minimal models for a KB with free occurrences of typicality in the propositional case was observed in [10] for Propositional Typicality Logic (PTL). The following is an example KB in SROEL ( /intersectionsq , × ) R T with alternative minimal canonical models having incomparable rank assignments. Example 3. Let K = ( TBox , RBox , ABox ) , where RBox = ABox = ∅ and TBox contains the inclusion ∃ U. ( A /intersectionsq T ( /latticetop )) /intersectionsq∃ U. ( B /intersectionsq T ( /latticetop )) /subsetsqequal ⊥ meaning that it is not the case that an A element and a B element may have both rank 0. Indeed, in the minimal canonical models of this knowledge base either A has rank 0 and B rank 1 or vice-versa. ## 4 Deciding rational entailment in polynomial time While instance checking in SROEL ( /intersectionsq , × ) R T under minimal entailment is Π P 2 -hard, in this section we prove that instance checking under rational entailment can be decided in polynomial time for normalized KBs, by defining a translation of a normalized KB into a set of Datalog rules, whose grounding is polynomial in the size of the KB. In particular, we extend the Datalog materialization calculus for SROEL ( /intersectionsq , × ) , proposed by Kr¨ otzsch [41], to deal with typicality concepts and with instance checking under rational entailment in SROEL ( /intersectionsq , × ) R T . The calculus in [41] uses predicates inst ( a , C ) (whose meaning includes: the individual a is an instance of concept name C , see [42] for details), triple ( a , R , b ) ( a is in relation R with b ), self ( a , R ) ( a is in relation R with itself). To map a SROEL ( /intersectionsq , × ) R T KB to a Datalog program, we add predicates to represent that: an individual a is a typical instance of a concept name ( typ ( a , C ) ); the ranks of two individuals a and b are the same ( sameRank ( a , b ) ); the rank of a is less or equal than the one of b ( leqRank ( a , b ) ). Besides the constants for individuals in N I (which are assumed to be finitely many), the calculus in [41] exploits auxiliary constants aux A /subsetsqequal∃ R.C (one for each inclusion of the form A /subsetsqequal ∃ R . C ) to deal with existential restriction. We also need to introduce an auxiliary constant aux C for any concept T ( C ) occurring in the KB or in the query, used as a representative typical C , in case C is non-empty. Given a normalized KB K = ( TBox , RBox , ABox ) and query Q of the form C ( a ) or T ( C )( a ) , where C is a concept name in the normalized KB, the Datalog program for instance checking in SROEL ( /intersectionsq , × ) R T , i.e. for querying whether K | = sroelrt Q , is a program Π ( K ) , the union of: 1. Π K , the representation of K as a set of Datalog facts, based on the input translation in [41]; 2. Π IR , the inference rules of the basic calculus in [41]; 3. Π RT , containing the additional rules for reasoning with typicality in SROEL ( /intersectionsq , × ) R T . Aquery Q of the form T ( C )( a ) , or C ( a ) , is mapped to a goal G Q of the form typ ( a , C ) , or inst ( a , C ) . Observe that restricting queries to concept names is not a severe restriction as an arbitrary query C ( b ) can be replaced by a query A ( b ) with A a new concept name, by adding C /subsetsqequal A to the TBox [1] and, of course, normalizing this inclusion when normalizing TBox. We define Π ( K ) in such a way that G Q is derivable in Datalog from Π ( K ) (written Π ( K ) /turnstileleft G Q ) if and only if K | = sroelrt Q . Π K includes the result of the input translation in section 3 in [41] where nom ( a ) , cls ( A ) , rol ( R ) are used for a ∈ N I , A ∈ N C , R ∈ N R , and, for example: - -subClass ( a , C ) , subClass ( A , c ) , subClass ( A , C ) are used for C ( a ) , A /subsetsqequal { c } , A /subsetsqequal C ; - -subEx ( R , A , C ) is used for ∃ R.A /subsetsqequal C ; and similar statements represent other axioms in the normalized KB. The following is the additional mapping for the extended syntax of the SROEL ( /intersectionsq , × ) R T normal form (note that no mapping is needed for assertions T ( C )( a ) , as they do not occur in a normalized KB): ``` ``` Also, we need to add top ( /latticetop ) and cls ( /latticetop ) to the input translation, as well as facts auxtc ( aux C , C ) to relate aux C constants to the corresponding concept for all C s such that T ( C ) occurs in the normalized KB, and, additionally, auxtc ( aux /latticetop , /latticetop ) . Π IR contains all the inference rules from [41] 1 : ``` ``` 1 Here, u, v, x, y, z, w , possibly with suffixes, are variables. ``` ``` Note that 'statements inst ( a, b ) , with a and b individuals, encode equality of a and b ' [42]. Π RT , the set of rules to deal with typicality, contains rules for supTyp and subTyp axioms, and rules that deal with the rank of domain elements. In the rules, x, y, z, Aux, A,B,C are all Datalog variables. ``` ``` Rules ( SupTyp , SubTyp ) deal with the corresponding statements, ( Refl ) corresponds to the reflexivity property (see Section 2), ( A0 -A3 ) encode properties of ranked models: if there is a C element, there must be a typical C element ( A0 ) ; a typical B element has a rank less or equal to the rank of any B element ( A1 ) ; two elements which are both typical A elements have the same rank ( A2 ) ; if x is a B element and has the same rank as a typical B element, x is also a typical B element ( A3 ) . Rules ( B1 -B6 ) define properties of rank order. In particular, by ( B6 ) , two constants that correspond to the same domain element have the same rank. Observe that the semantic properties of rational consequence relation introduced in Section 2 are enforced by the specification above. Consider, for instance, ( S -CM ) . Suppose that subTyp ( A , B ) and subTyp ( A , C ) are in Π K (as T ( A ) /subsetsqequal B , T ( A ) /subsetsqequal C are in K ) and that D is a concept name defined to be equivalent to A /intersectionsq B in K . Suppose that typ ( a , D ) holds. One can infer typ ( a , A ) and hence inst ( a , C ) , i.e., typical A /intersectionsq B 's inherit from typical A 's the property of being C 's (the inference for Paul in Example 1). In fact, typ ( a , A ) is inferred showing that a (who is a typical D and an A , as it is a D ) and aux A (who is a typical A , by ( A0 ) , and a D , since all the typical A 's are also B 's and hence A /intersectionsq B 's) have the same rank. In fact, using ( A1 ) twice, one can conclude both leqRank ( a , aux A ) and leqRank ( aux A , a ) so that, by ( B5 ) , sameRank ( a , aux A ) . Then, by ( A3 ) , we infer typ ( a , A ) . With rule ( subTyp ) , from typ ( a , A ) and subTyp ( A , C ) , we conclude inst ( a , C ) . Reasoning in a similar way, one can see that properties ( S -RM ) and ( S -LLE ) are also enforced by the rules above. For ( S -RM ) : from the fact that there is a domain element a which is a T ( A ) and a C element (i.e. typ ( a , A ) and inst ( a , C ) hold), and from the fact that there is a b whois a typical A /intersectionsq C element (i.e. that typ ( b , D ) holds, for some concept D equivalent to A /intersectionsq C ), we can conclude that b is also a typical A element (i.e. typ ( b , A ) holds). Inference in SROEL ( /intersectionsq , × ) already takes care of the semantic properties of conjunctive consequences ( S -And ) and right weakening ( S -RW ) . Theorem 2. For a SROEL ( /intersectionsq , × ) R T KB in normal form K , and a query Q of the form T ( C )( a ) or C ( a ) , K | = sroelrt Q if and only if Π ( K ) /turnstileleft G Q . Proof. For completeness, we procede by contraposition, similarly to [42], Lemma 3. Assume that inst ( a , C ) (respectively, typ ( a , C ) ) is not derivable from Π ( K ) . Let J be the minimal Herbrand model of the Datalog program Π ( K ) ; then inst ( a , C ) /negationslash∈ J (resp. typ ( a , C ) /negationslash∈ J ). From J we build a ranked model M = ( ∆,<, · I ) for K such that C ( a ) (respectively, T ( C )( a ) ) is not satisfied in M . As in [42], we can build the domain ∆ of M from the set Const including all the name constants c ∈ N I occurring in the ASP program Π ( K ) as well as all the auxiliary constants, then defining an equivalence relation ≈ over constants as the reflexive, symmetric and transitive closure of the relation { ( c, d ) | inst ( c, d ) ∈ J , for c ∈ Const and d ∈ N I } . Let [ c ] = { d | d ≈ c } denote the equivalence class of c ; we define the domain ∆ of the interpretation M as the set including the equivalence classes [ c ] for the c ∈ N I and, possibly, additional domain elements for auxiliary constants: ∆ = { [ c ] | c ∈ N I }∪{ w A /subsetsqequal∃ R.C 1 , w A /subsetsqequal∃ R.C 2 | inst ( aux A /subsetsqequal∃ R.C , e ) ∈ J for some e and there is no d ∈ N I such that aux A /subsetsqequal∃ R.C ≈ d } ∪{ z 1 C , z 2 C | inst ( aux C , e ) ∈ J for some e and there is no d ∈ N I such that aux C ≈ d } . Two copies of auxiliary constants are introduced, as in [42], to handle Self statements. For each element e ∈ ∆ , we define a projection ι ( e ) to Const as follows: (i) ι ([ c ]) = c ; (ii) ι ( w A /subsetsqequal∃ R.C i ) = aux A /subsetsqequal∃ R.C , i=1,2; (iii) ι ( z i C ) = aux C , i = 1 , 2 . J contains all the details about the interpretation of concepts and roles, from which an interpretation M can be defined as follows: - -∀ c ∈ N I , c I = [ c ] ; - -∀ d ∈ ∆ , d ∈ A I iff inst ( ι ( d ) , A ) ∈ J ; - -∀ d , e ∈ ∆ , ( d , e ) ∈ R I iff ( triple ( ι ( d ) , R , ι ( e )) ∈ J and d = e ) or ( self ( ι ( d ) , R ) ∈ J and d = e ). /negationslash We define a relation < ′ over constants, letting x < ′ y iff there is a concept name C , s.t. typ ( x , C ) , inst ( y , C ) ∈ J and typ ( y , C ) /negationslash∈ J ; we can show that its transitive closure < + is a strict partial order. To see that < + is irreflexive, we procede by contradiction. If there were a chain x < ′ y 1 < . . . < ′ y n = x , so that x < + x , by definition of < ′ , the facts leqRank ( x , y 1 ) , . . . , leqRank ( y n -1 , x ) would be in J and, by applications of (B4) and (B5), sameRank ( x , y 1 ) would also be in J . As x < ′ y 1 , there is some concept name C , s.t. typ ( x , C ) , inst ( y 1 , C ) ∈ J and typ ( y 1 , C ) /negationslash∈ J , but, from typ ( x , C ) , inst ( y 1 , C ) and sameRank ( x , y 1 ) , by (A3), typ ( y 1 , C ) must be in J as well, a contradiction. Similarly, one can see that < + is compatible with the sameRank predicate in J (i.e., it is not the case that a < + b and sameRank ( a, b ) ) and with the ≈ equivalence relation between constants (i.e., it is not the case that a < + b and a ≈ b ) so that < + can be extended to a modular partial order over the domain ∆ as follows. First, a partial ordering over elements in ∆ is defined, letting e < d iff ι ( e ) < + ι ( d ) , for all e, d ∈ ∆ (where the definition does not depend on the choice of the representative element in a class). Then the elements in ∆ are partitioned into the sets Rank 0 , . . . , Rank n , where Rank i (the set of domain elements of rank i ) is defined by induction on i , as follows: Rank 0 contains all the elements x ∈ ∆ such that there is no y ∈ ∆ with y < x ; Rank i contains all the elements x ∈ ∆ -( Rank 0 ∪ . . . ∪ Rank i -1 ) such that there is no y ∈ ∆ -( Rank 0 ∪ . . . ∪ Rank i -1 ) with y < x . We let n be the least integer such that ∆ -( Rank 0 ∪ . . . ∪ Rank n ) = ∅ . In M we let k M ( x ) = i if x ∈ Rank i , for all x ∈ ∆ and i = 1 , n . It can be shown that M is a model of K and it does not satisfy C ( a ) (respectively, T ( C )( a ) ). The proof that M is a model of K , i.e. it satisfies all the axioms in KB, is the same as in [42] (see Lemma 2), apart from the fact that we have to consider the additional axioms A /subsetsqequal T ( B ) and T ( B ) /subsetsqequal C (observe that an assertion T ( C )( a ) cannot occur in the ABox, as K is in normal form). For A /subsetsqequal T ( B ) in K , we have supTyp ( A , B ) ∈ J . Let us assume that d ∈ A I . We want to prove that d ∈ ( T ( B )) I . By construction inst ( ι ( d ) , A ) ∈ J . By rule (SupTyp) , typ ( ι ( d ) , B ) ∈ J . By rule (Refl) , inst ( ι ( d ) , B ) ∈ J , i.e., d ∈ B I . Let us assume k M ( d ) = h . To show that d is a typical B , we have to show that, for all the domain elements e with rank j < h , e /negationslash∈ B I . Suppose, by contradiction, that there were an e such that e ∈ B I and k M ( e ) < k M ( d ) . By construction, it would be that inst ( ι ( e ) , B ) ∈ J and that ι ( e ) < + ι ( d ) . Hence, there would be a sequence ι ( e ) < ′ y 1 < . . . < ′ y n = ι ( d ) ( n ≥ 1 ) and, by definition of < ′ , leqRank ( ι ( e ) , y 1 ) , . . . , leqRank ( y n -1 , ι ( d )) would be in J . By (B4) leqRank ( ι ( e ) , ι ( d )) would be in J . Also, from inst ( ι ( e ) , B ) ∈ J and typ ( ι ( d ) , B ) ∈ J , by (A1), leqRank ( ι ( d ) , ι ( e )) ∈ J . Therefore, by (A2), sameRank ( ι ( e ) , ι ( d )) would be in J . This contradicts the fact that ι ( e ) < + ι ( d ) (as < + must be compatible with sameRank ), and hence it contradicts the hypothesis that k M ( e ) < k M ( d ) . For T ( B ) /subsetsqequal C in K , we have subTyp ( B , C ) ∈ J . Let d ∈ ( T ( B )) I . We have to prove that d ∈ C I . Let k M ( d ) = h . As d ∈ ( T ( B )) I , d ∈ B I and, for all e ∈ ∆ such that k M ( e ) = j < h , e /negationslash∈ B I . From d ∈ B I , by the definition of M , inst ( ι ( d ) , B ) ∈ J . In the case typ ( ι ( d ) , B ) ∈ J , by (SubTyp) inst ( ι ( d ) , C ) ∈ J and, by definition of M , d ∈ C I . We show that the case when typ ( ι ( d ) , B ) /negationslash∈ J cannot occur. Suppose by contradiction that typ ( ι ( d ) , B ) /negationslash∈ J . Consider the auxiliary constant aux B and let aux I B ∈ Rank r , i.e. k M ( aux I B ) = r . By rule (A0), from inst ( ι ( d ) , B ) ∈ J , we have typ ( aux B , B ) ∈ J and, from ( Refl ) , inst ( aux B , B ) ∈ J . From typ ( aux B , B ) ∈ J and inst ( ι ( d ) , B ) ∈ J , as we have assumed typ ( ι ( d ) , B ) /negationslash∈ J , by definition of < ′ , we have aux B < ′ ι ( d ) , and hence aux B < + ι ( d ) . Therefore, by construction of M , aux I B < d . Also from inst ( aux B , B ) ∈ J , by construction, we have aux I ∈ B I , which contradicts the hypothesis that d ∈ ( T ( B )) I . We have proved that M is a model of KB. To conclude the proof, let us consider the query Q . If Q = C ( a ) , inst ( a, C ) /negationslash∈ J then, by definition of M , a I /negationslash∈ C I , so that C ( a ) is not satisfied in M . If Q = T ( C )( a ) , typ ( a, C ) /negationslash∈ J . We prove that a I /negationslash∈ ( T ( C )) I . We consider 2 cases: inst ( a, C ) /negationslash∈ J and inst ( a, C ) ∈ J . In the first case, by definition of M , a I /negationslash∈ C I and hence a I /negationslash∈ ( T ( C )) I . In the second case, from inst ( a, C ) ∈ J , by (A0) typ ( aux C , C ) ∈ J . As typ ( a, C ) /negationslash∈ J , by definition of < ′ we have: aux C < ′ a . Hence, aux C < + a and, in M , aux I C < a I . As by (Refl) inst ( aux C , C ) ∈ J , in M aux I B ∈ C I . Therefore, a I /negationslash∈ ( T ( C )) I . This concludes the proof of Completeness. Proving the soundness of the Datalog encoding requires showing that, if Π ( K ) /turnstileleft G Q , for a query Q of the form T ( C )( a ) or C ( a ) , then, Q is a logical consequence of K . The proof is similar to the proof of Lemma 1 in [42]. First we associate to each constant c of the Datalog program Π ( K ) a concept expression κ ( c ) as follows: ``` ``` The following statements can be proved by induction on the height of the derivation tree of each atom from the program Π ( K ) : - if Π ( K ) /turnstileleft inst ( c , A ) , for A ∈ N C , then K | = sroelrt κ ( c ) /subsetsqequal A ; - if Π ( K ) /turnstileleft inst ( c , d ) , for d ∈ N I , then K | = sroelrt κ ( c ) /subsetsqequal { d } ; - if Π ( K ) /turnstileleft triple ( c , R , d ) , then K | = sroelrt κ ( c ) /subsetsqequal ∃ R.κ ( d ) ; - if Π ( K ) /turnstileleft self ( c , R ) , for A ∈ N C , then K | = sroelrt κ ( c ) /subsetsqequal ∃ R . Self ; - if Π ( K ) /turnstileleft typ ( c , A ) , then K | = sroelrt κ ( c ) /subsetsqequal T ( A ) ; - -if Π ( K ) /turnstileleft sameRank ( c , d ) then for all models M of K , k M ( x ) = k M ( y ) , ∀ x ∈ κ ( c ) , ∀ y ∈ κ ( d ) ; - if Π ( K ) /turnstileleft leqRank ( c , d ) then, for all models M of K , k M ( x ) ≤ k M ( y ) , ∀ x ∈ κ ( c ) , ∀ y ∈ κ ( d ) ; where, in all the items above, κ ( c ) and κ ( d ) are nonempty in all the models of K . The proof of the first four items goes through as in the proof of Lemma 1 in [42], with few additions for the first case, as there are additional inference rules (namely (SubTyp) and (Refl) ) to derive inst ( c , A ) . As an example, let us consider the case when inst ( c , A ) is derived from Π ( K ) by applying rule (SubTyp) . Then SubTyp ( B , A ) and typ ( c , B ) must be derivable and the height of their derivation tree is lower. By inductive hypothesis, K | = sroelrt κ ( c ) /subsetsqequal T ( B ) . Also, as SubTyp ( B , A ) is in the input translation, T ( B ) /subsetsqequal A must be in K . Therefore, it follows that K | = sroelrt κ ( c ) /subsetsqequal A . If inst ( c , A ) is derived from Π ( K ) by applying the rule (Refl) , then typ ( c , A ) is derived with a lower derivation tree. By inductive hypothesis, K | = sroelrt κ ( c ) /subsetsqequal T ( A ) and, hence, K | = sroelrt κ ( c ) /subsetsqequal A . Let us now consider the fifth item. Assume that Π ( K ) /turnstileleft typ ( c , A ) ; typ ( c , A ) can be derived using one of the rules (SupTyp), (A0) or (A3) . The first two cases are trivial. If rule (A3) is used to derive typ ( c , A ) , then sameRank ( c , d ) , inst ( c , A ) , typ ( d , A ) are derived with a lower derivation tree. By inductive hypothesis, K | = sroelrt κ ( c ) /subsetsqequal A , K | = sroelrt κ ( d ) /subsetsqequal T ( A ) and, for all the models M of K , the rank of all instances of κ ( c ) is the same as the rank of all instances of κ ( d ) . As all the κ ( c ) are A elements and have the same rank as the typical A elements, then K | = sroelrt κ ( c ) /subsetsqequal T ( A ) . Π ( K ) contains a polynomial number of rules and exploits a polynomial number of concepts in the size of K , hence instance checking in SROEL ( /intersectionsq , × ) R T can be decided in polynomial time using the calculus in Datalog. The encoding can be processed, e.g., in an ASP solver such as Clingo or DLV (with the proper capitalization of variables); computation of the (unique, in this case) answer set takes a negligible time for KBs with a hundred assertions (half of them with T ). Exploiting the approach presented in [41], a version of the Datalog specification where predicates inst , typ , triple , self , sameRank , leqRank have an additional parameter (and is therefore less efficient than the previous one, although polynomial) can be used to check subsumption for SROEL ( /intersectionsq , × ) R T . Indeed, to check a subsumption A /subsetsqequal B from a KB K , one can check that, for some new individual name c , B ( c ) is entailed from the KB K ∪ { A ( c ) } . Following [41] the class B can be used as the new individual name c . In the ternary predicate inst ( a , C , B ) , the additional parameter B stands for the assumption that the new individual B is an instance of the concept B . This is encoded by adding the rule inst ( B , B , B ) ← cls ( B ) to the inference rules (and similarly for the other predicates). ## 5 Rational Closure in Datalog plus Stratified Negation Given a KB K , the model constructed in the completeness proof from the minimal Herbrand Model J of the encoding Π ( K ) is not in general a minimal model of K . Consider the following example. Example 4. Let K = ( TBox,RBox,ABox ) , with RBox = ∅ , ABox = { T ( D )( a ) } , and TBox containing the following inclusions: (1) T ( A ) /intersectionsq T ( B ) /subsetsqequal ⊥ , (2) A /intersectionsq B /subsetsqequal D , (3) D /subsetsqequal A , (4) D /subsetsqequal B . From Π ( K ) we can derive samerank ( aux D , a ) and, from the definition of < we get: aux /latticetop < aux A (in fact, typ ( aux /latticetop , /latticetop ) and inst ( aux A , /latticetop ) are in J while typ ( aux A , /latticetop ) /negationslash∈ J ), aux /latticetop < aux B , aux A < aux D , aux B < aux D , aux A < a , aux B < a . Using the construction in the completeness proof, we would let ∆ = { [ aux /latticetop ] , [ aux A ] , [ aux B ] , [ aux D ] , [ a ] } , Rank 0 = { [ aux /latticetop ] } ; Rank 1 = { [ aux A ] , [ aux B ] } and Rank 2 = { [ aux D ] , [ a ] } . This is not a minimal model of K . In fact, we can lower the rank of [ aux A ] and [ aux B ] to 0 , without changing the evaluation of atomic concepts, roles and individual constants (as defined in the model, and in J ) and we still obtain a model of K . Similarly, the rank of [ aux D ] and [ a ] can be lowered to 1 . The resulting model is a minimal model of K . For simple SROEL ( /intersectionsq , × ) R T knowledge bases, i.e., for KBs where the typicality operator only occurs on the left hand side of inclusions in the Tbox, and we assume moreover it does not occur in the Rbox nor in the Abox, the rational closure of TBox can be obtained, adapting the construction in [32] (Definitions 21 and 23). Such a construction can be reformulated replacing the exceptionality check and the entailment in ALC + T R with the ones in SROEL ( /intersectionsq , × ) R T . The idea is that of assigning the lowest possible rank to each concept. A concept with rank 0 must have instances which do not violate any defeasible inclusions. If a concept C has a rank higher than 0 , then all its instances necessarily violate some defeasible inclusions. This concept is exceptional with respect to K , as it cannot be satisfied by the most normal domain elements in some (minimal and canonical) model of K . The iterative construction of the rational closure builds on this notion of exceptionality, by repeatedly selecting exceptional concepts and their typicality inclusions. Formally, in [32], a concept C is defined as exceptional for a knowledge base K iff T ( /latticetop ) /subsetsqequal ¬ C is rationally entailed by K . As negation is not available in SROEL ( /intersectionsq , × ) R T , we reformulate exceptionality as follows: a concept C is exceptional for a knowledge base K iff K | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal ⊥ . An inclusion T ( C ) /subsetsqequal D is exceptional for K if C is exceptional for K . The set of inclusions that are exceptional for K is denoted as E ( K ) . Given K = ( Tbox, Rbox, Abox ) , a sequence E 0 = K,E 1 , . . . , E n of knowledge bases can be defined letting, for i > 0 : E i = ( Tbox i , Rbox, Abox ) , where Tbox i = E ( E i -1 ) ∪ { C /subsetsqequal D ∈ Tbox, T does not occur in C } . For all i , Tbox i -1 ⊇ Tbox i . Being K finite, there is a least finite n ≥ 0 such that, for all m > n , Tbox m = Tbox n (as special case, they are all ∅ ). The construction can then be limited to such n , which is reached if Tbox n +1 = Tbox n . A concept C has rank i , i.e., rank ( C ) = i , if i the least number such that C is not exceptional for E i . If C is exceptional for all E i , we set rank ( C ) = ∞ . The rational closure of Tbox for a knowledge base K = ( Tbox, Rbox, Abox ) is defined as: Tbox = { T ( C ) /subsetsqequal D | either rank ( C ) < rank ( C /intersectionsq ¬ D ) or rank ( C ) = ∞}∪{ C /subsetsqequal D | K | = sroelrt C /subsetsqequal D } . Actually, C /intersectionsq ¬ D is not in the language of SROEL ( /intersectionsq , × ) R T , but as we shall see, the condition involving it will be reformulated accordingly. For instance, in Example 1, the rational closure construction would assign rank 0 to concepts Student , Student /intersectionsq Italian , Student /intersectionsq Young , MathHater , rank 1 to Student /intersectionsq ¬ MathHater , Student /intersectionsq Nerd , and rank 2 to Student /intersectionsq Nerd /intersectionsq¬ MathLover . In the following we define rules for computing the rational closure construction, using a variant of the calculus in section 4 (similar to its variant for subsumption) and stratified negation. The set of rules to infer whether inclusions of the form T ( C ) /subsetsqequal D , with C, D ∈ N C , are in the rational closure of the TBox for a simple SROEL ( /intersectionsq , × ) R T knowledge base K, is a set Π RT ( K ) which is the union of: - 1 Π K and Π IR as in section 4; - 2 Π ′ RT which is Π RT in section 4 omitting rule ( SupTyp ) , given that K is a simple KB; - 3 Π RC which contains the rules for rational closure as described below. Π RC contains rules to define exceptionality of a concept C wrt a KB E i , which, as said before, means E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal ⊥ , for all the concepts C such that T ( C ) occurs in the program or in a typicality subsumption T ( C ) /subsetsqequal D to be checked. For all such Cs we assume to have a statement auxtc ( aux C , C ) , and we define the set of such Cs with a rule t cls ( C ) ← auxtc ( Aux , C ) . The entailment E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal ⊥ is verified checking whether, for a new constant C (the same name of the class is reused as constant name, as in the calculus for subsumption in [41] mentioned at the end of section 4), it holds that E i ∪ { T ( /latticetop )( C ) , C ( C ) } | = sroelrt ⊥ ( C ) . Similarly to the calculus for subsumption, we use a version of the basic calculus defining predicates inst h , self h , triple h , typ h , leqRank h , sameRank h , which correspond to the ones in the basic calculus in section 4, with two additional parameters, one for the concept C in the hypotheses T ( /latticetop )( C ) , C ( C ) and one for an integer i identifying E i in the sequence of KBs. Then, the idea is that inst h ( y , z , C , i ) holds when E i ∪ { T ( /latticetop )( C ) , C ( C ) } | = sroelrt z ( y ) . Π RC includes the following rules for determining the exceptionality of concepts for each E i : - ) ``` ``` where: ( C1 ) defines the possible rank values for concepts, given that an assertion upperbound ( n ) is added to the input translation Π ( K ) , where n is one more the number of T ( C ) occurring in Tbox ; ( C2 ) defines exceptionality of C for E i ; ( C3 , C4 ) define which inclusions T ( C ) /subsetsqequal D belong to E ( E i -i ) and then to E i ; ( C5 , C6 ) provide the assumptions { T ( /latticetop )( C ) , C ( C ) } for reasoning in E i ∪ { T ( /latticetop )( C ) , C ( C ) } . Additionally, Π RC contains a version of the rules in Π ′ RT where predicates inst , self , triple , typ , leqRank , sameRank are replaced by inst h , self h , triple h , typ h , leqRank h , sameRank h respectively, with two additional parameters D and I ; in all rules t cls ( D ) , possrank ( I ) is added to the antecedent, and the rule derived from ( subTyp ) is: <!-- formula-not-decoded --> i.e., it uses subTyp ( A , C , I ) rather than subTyp ( A , C ) , given that reasoning is in E i , not in K . Let Π Pos RT ( K ) be the set of all the rules in Π RT ( K ) introduced so far, which are all positive Datalog rules. It is easy to see that the following proposition holds: Proposition 2. For a SROEL ( /intersectionsq , × ) R T KB in normal form K : - (1) Π Pos RT ( K ) /turnstileleft subTyp ( C , D , i ) iff T ( C ) /subsetsqequal D ∈ E i . (2) Π Pos RT ( K ) /turnstileleft inst h ( C , D , C , i ) iff E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal D ; Pos is excep- - (3) Π RT ( K ) /turnstileleft exceptional ( C , i ) iff E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal ⊥ (i.e., C tional for E i ) Proof. (Sketch) The proof can be done by induction on i . For i = 0 , (1) holds, as by rule (C3) subTyp ( C , D , 0 ) is derivable when subTyp ( C , D ) is derivable, i.e, by the input translation, when T ( C ) /subsetsqequal D ∈ K . Also, (C3) is the only rule to define subTyp ( C , D , 0 ) , which is not derivable if subTyp ( C , D ) is not (that is when T ( C ) /subsetsqequal D /negationslash∈ K ). Also, by construction, E 0 = K . Item (2) follows according to the same considerations given for the calculus for subsumption in [41]. As a difference, here the further hypothesis T ( /latticetop )( C ) is added besides the hypothesis C ( C ) (see rules (C5) and (C6)). For item (3), exceptional ( C , i ) is derivable by rule (C2) if and only if for some Z , inst h ( C , Z , C , i ) and bot ( Z ) are derivable. In this case, by (2), E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal Z . Furthermore, as bot ( Z ) is derivable, Z /subsetsqequal ⊥ must be in K , and hence E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal ⊥ . The inductive case can be easily proved. Π RC also contains the following rules for computing the rank of concepts: ``` ( C7 ) rank( C, 0) <- t_cls( C ), not exceptional( C, 0) ( C8 ) rank( C, I ) <- t_cls( C ), posssrank( I ), exceptional( C, I - 1), not exceptional( C, I ) ( C9 ) newNonEx( I ) <- t_cls( C ), rank( C, I) ( C10 ) fixp( I ) <- posssrank( I ), I > 0 , not newNonEx( I ) ( C11 ) fixp( I ) <- posssrank( I ), fixp( I - 1) ( C12 ) inf_rank( C ) <- fixp( I ), exceptional( C, I ) ``` where, according to the definition of rank, a concept C has rank 0 if C is not exceptional for E 0 , i.e., by Proposition 2, if exceptional ( C , 0 ) is not derivable (rule (C7)), and similarly for a rank i > 0 (rule (C8)). Predicate newNonEx ( i ) is true if there is some new non exceptional concept at i , which was exceptional at i -1 (i.e. there is some concept with rank i ). If not, the iteration has reached a fixpoint at i (and fixp ( i ) holds by (C10)), and the remaining concepts C which are exceptional for E i , for some i such that fixp ( i ) holds, have an infinite rank and, by (C12), inf rank ( C ) is derivable. Clearly it cannot be the case that both inf rank ( C ) and rank ( C , i ) hold for some i . Finally, for defeasible subsumption queries, we introduce the new predicate inrc ( x , y ) and the rules: ``` ( inrc1 ) inrc( C, D ) <- t . cls( C ), cls( D ), rank( C, I ), inst . h( C, D, C, I ) ( inrc2 ) inrc( C, D ) <- t . cls( C ), cls( D ), inf . rank( C ) ``` which determine whether T ( C ) /subsetsqequal D , with C, D ∈ N C , is in Tbox , the rational closure of Tbox for the knowledge base. Rule ( inrc1 ) is for the case rank ( C ) < rank ( C /intersectionsq ¬ D ) and deserves some comment. Given that rank ( C ) = i , it should be checked that rank ( C /intersectionsq¬ D ) > i . rank ( C /intersectionsq¬ D ) could either be equal to i or larger. It is equal to i iff C /intersectionsq¬ D is not exceptional in E i and, then, it is > i iff C /intersectionsq¬ D is exceptional in E i , i.e., E i | = sroelrt T ( /latticetop ) /intersectionsq C /intersectionsq ¬ D /subsetsqequal ⊥ , i.e., E i | = sroelrt T ( /latticetop ) /intersectionsq C /subsetsqequal D , which, by Proposition 2, can indeed be verified by checking that inst h ( C , D , C , I ) is derivable. To avoid the derivation of an atom inrc ( C , D ) , for each defeasible inclusion T ( C ) /subsetsqequal D belonging to the rational closure of K , for all C, D ∈ N C , a condition def subs ( C , D ) can be introduced in the antecedent of rules ( inrc1 ) and ( inrc2 ) , and facts def subs ( C , D ) added for the subumptions T ( C ) /subsetsqequal D we are interested in checking, as well as the fact t cls ( C ) , in case T ( C ) does not occur in K . Observe that the resulting program Π RC contains negated literals and is stratified [48], i.e., the predicates in the program can be partitioned into a finite number of pairwise disjoint sets P 0 , . . . , P k , in such a way that, for each rule whose head is in P i , each predicate occurring in a positive literal in the body must belong to some P j with j ≤ i , and each predicate occurring in a negative literal in its body must belongs to some P j with j < i . Indeed, three pairwise disjoint sets of predicates P 0 , P 1 and P 2 can be defined , where P 0 contains all the predicates in Π Pos RT ( K ) , P 1 contains predicates rank and newNonEx , and P 2 contains predicates fixp , inf Rank , inrc1 and inrc2 . Thenon-disjunctive, stratified Datalog program Π RT ( K ) has a unique perfect model, coinciding with the unique stable model of the program [48]. When restricted to the predicates in P 0 , occurring in the positive part Π Pos RT ( K ) , the unique stable model of Π RT ( K ) coincides with the minimal model of Π Pos RT ( K ) (i.e. with the set of facts derivable from Π Pos RT ( K ) in Datalog), as a consequence of a general property of modularized disjunctive Datalog programs in [20] (Lemma 5.1). The fact that a concept C has rank i ( rank ( C , I ) ), as well as the existence of a concept with rank i ( newNonEx ( I ) ), and the fact that the iteration has reached a fixedpoint at i ( fixp ( I ) ) can then all be computed stratum by stratum according to the rules (C7)-(C12). Their correctness is evident from their definition, and we omit a formal proof. For K in Example 4, the program Π RT ( K ) has a unique stable model in which rank ( aux /latticetop , 0 ) , rank ( aux A , 0 ) , rank ( aux B , 0 ) , rank ( aux D , 1 ) , rank ( a , 1 ) hold. Observe that computing the ranks of all concepts C such that T ( C ) occurs in the KB (or in the query) requires a quadratic number of exceptionality checks in the size of the KB (as the maximum rank value that can be assigned to a concept is bounded by the number of typicality inclusions in the KB). Each exceptionality check requires polynomial time, using the above mentioned variant of polynomial calculus for subsumption, by a call to predicate inst h ( C, Z, C, I ) . As observed, the computation of the ranking can be done stratum by stratum and requires polynomial time. The correspondence between the rational closure construction and the canonical minimal model semantics in [32] does not extend to all the constructs in SROEL ( /intersectionsq , × ) R T and, specifically, the canonical model semantics is not adequate for dealing with nominals. In particular, there are knowledge bases with no canonical model and knowledge bases with more than one minimal canonical model (as the knowledge base in Example 3). However, in many cases, the rational closure of a KB with no canonical model is still meaningful. As an example, observe that the TBox consisting of the rules (a)-(f) in Example 1 is simple, but has no canonical model (in fact, although the concepts { black } /intersectionsq MathHather and { black } /intersectionsq MathLover are both consistent with K , there is no model of K in which they both have an instance). However, the rational closure of this TBox is consistent, and entails, for instance, that all the typical young Italians have black hair. In particular, the concepts student and young Italian are given rank 0 , while nerd student has rank 1 and nerd student and math hater has rank 2 . A less restrictive semantic requirement to give meaning also to KBs containing nominals has been considered in [33], where T -minimal models are introduced, corresponding to the minimal models among the ones which contain at least one instance of any consistent concept occurring within the typicality operator in the KB. We refer to [33] for a detailed description of this semantics and of its relation with the minimal canonical model one. The two semantics coincide when minimal canonical models of the KB exist and give to all the concepts occurring in the T operator the same rank computed by the rational closure construction. One can expect that the correspondence among the rational closure and the T -minimal model semantics extends to a larger fragment of the language including the TBox (a)-(f) above, for which a unique T -minimal model exists. While in this paper we do not address the issue of determining such a fragment and establishing the correspondence, we notice that checking the consistency of the rational closure provides a simple way to identify the KB for which the rational closure construction is meaningful. The consistency of the rational closure can be easily determined using the materialization calculus. The following rules: ``` ( SameRank rc1 ) sameRank( A _ { C } , A _ { D } ) <- auxtc ( A _ { C } , C ) , auxtc ( A _ { D } , D ) , r rank ( C , I ) , rank ( D , I ) . ( LeqRank rc2 ) leqRank ( A _ { C } , A _ { D } ) <- auxtc ( A _ { C } , C ) , auxtc ( A _ { D } , D ) , r rank ( C , I ) , rank ( D , J ) , I < J . ``` are added to Π RC to incorporate the information on the ranks computed by the rational closure construction in the materialization calculus. If the resulting program derives inst ( x , A ) for any concept A such that bot ( A ) ∈ Π K , then the rational closure of K is inconsistent, as the rank assignment computed by the rational closure does not correspond to any model of the KB (which can be proved, by a simple generalization of the soundness proof in Theorem 2). Note that, if the inclusion ∃ U. ( { a }/intersectionsq T ( /latticetop )) /intersectionsq∃ U. ( { b }/intersectionsq T ( /latticetop )) /subsetsqequal ⊥ (similar to the inclusion in the multiple extension Example 3) were added to the KB from Example 1, with the TBox consisting of rules (a)-(f) as above, the computed ranks would not change w.r.t. those given above. However, if T ( { a } ) /subsetsqequal C and T ( { b } ) /subsetsqequal D were added, the rational closure would become inconsistent as it would assign to both concepts { a } and { b } a rank, namely 0 , but no model of the KB exists which such ranks. For a consistent KBs in SROEL ( /intersectionsq , × ) R T whose rational closure is inconsistent, two options are available: either to reason (skeptically) on the alternative T -minimal models of the KB (if any) by exploiting the ASP encoding of the T -minimal model semantics in [33], or to take the inconsistency as a clue that there are potentially unresolved conflicts in the KB, concerning the inheritance of alternative defeasible inclusions from more general to more specific classes, to be resolved by modifying the KB (an approach adopted for the logic of overriding in [6]). ## 6 Related Work Among the recent nonmonotonic extensions of DLs are the formalisms for combining DLs with logic programming rules, such as for instance, [22,21,47,39] and Datalog +/[37]. DL-programs [22,21] support a loose coupling of DL ontologies and rule-based reasoning under the answer set semantics and the well-founded semantics; rules may contain DL-atoms in their bodies, corresponding to queries to a DL ontology, which can be modified according to a list of updates. In [39] a general DL language is introduced, which extends SROIQ with nominal schemas and epistemic operators according to the MKNF semantics [47], which encompasses prominent nonmonotonic rule languages, including ASP. In [6] a non monotonic extension of DLs is proposed based on a notion of overriding, supporting normality concepts and enjoying good computational properties, preserving the tractability of low complexity DLs, including EL ++ and DL -lite . In [11] the CKR framework is presented; it is based on SROIQ-RL , allows for defeasible axioms with local exceptions and exploits a translation to Datalog with negation. It is shown that instance checking in CKR reduces to (cautious) inference under the answer set semantics. Preferential extensions of low complexity DLs in the EL and DL-lite families have been studied in [29,30], based on preferential interpretations which are not required to be modular, and tableaux-based proof methods have been developed for them. In [30], for a preferential extension of EL ⊥ based on a minimal model semantics different from the one in this paper, it is shown that minimal entailment is EXPTIME-hard already for simple KBs, similarly to what happens for circumscriptive KBs [7]. The first notion of rational closure for DLs was defined by Casini and Straccia [14]; their rational closure construction for ALC directly uses entailment in ALC over a materialization of the KB. A variant of this notion of rational closure has been studied in [13]. To overcome the limitations of rational closure, in [16] an approach is introduced based on the combination of rational closure and Defeasible Inheritance Networks , while in [15] the lexicographic closure introduced by Lehmann [44] is extended to description logics. Furthermore, in [25] an extension of ALC + T with several typicality operators is proposed, each corresponding to a preference relation, and in [36] a refinement of the rational closure is developed, where models are equipped with several preference relations. Whether the presented approach can be extended to refinements of rational closure will be explored in future work. In [33] a rule based inference method for SROEL ( /intersectionsq , × ) R T minimal entailment based on model generation in ASP has been developed; here we exploit Datalog plus stratified negation to construct the rational closure of a KB. As discussed above, the two approaches are complementary. Related approaches are the work in [5] which characterizes skeptical c-inference as a constraint satisfaction problem, and the work in [17], who presents an inconsistency tolerant semantics for the Description Logic using preference weights and exploit ASP optimization for computing preferred interpretations. ## 7 Conclusions In this paper we have studied a rational extension SROEL ( /intersectionsq , × ) R T of the low complexity description logic SROEL ( /intersectionsq , × ) , which underlies the OWL EL ontology language, introducing a typicality operator. For general KBs, we have shown that minimal entailment in SROEL ( /intersectionsq , × ) R T is Π P 2 -hard. When free occurrences of typicality concepts in concept inclusions are allowed, alternative minimal models may exist with different rank assignments to concepts. In [10] this phenomenon has been analyzed in the context of PTL, considering alternative preference relations over ranked interpretations which coincide over simple KBs but, for general ones, define different notions of entailment satisfying alternative and possibly incompatible postulates. Building on the calculus for SROEL ( /intersectionsq , × ) in Datalog presented in [41], a calculus for instance checking and subsumption under rational entailment is defined, showing that these problems can be decided in polynomial time. A preliminary version of this result appeared in [34,35]. This calculus is extended to provide a polynomial construction of the rational closure of a knowledge base in SROEL ( /intersectionsq , × ) R T , using Datalog with stratified negation [48]. Although the minimal canonical model semantics provides a characterization for rational closure of simple SROEL ( /intersectionsq , × ) R T knowledge bases on the fragment of the language only including the constructs in ALC (by a result in [32]), a more general semantic characterization for a wider fragment of the language is still to be developed. In this respect, a promising semantics is the T -minimal model semantics proposed in [33]. Future work may also include optimizations, based on modularity as in [9], of the calculus for rational entailment, the development of a multi-preference construction to address the drawbacks of rational closure as the development of Abox minimization techniques. A further issue to understand is whether a calculus can be defined also for the preferential extensions of DLs in the EL family studied in [29,30], whose interpretations are not required to be ranked, as well as for the logics in the DL-lite family, for which inconsistency tolerant semantics have been developed [45,4]. Apart from providing a polynomial complexity upper bound, the encoding presented in this paper is intended to provide a way to integrate the use of SROEL ( /intersectionsq , × ) KBs under rational entailment with other kinds of reasoning that can be performed in ASP, and, by modifying the encoding, also to allow the experimentation of alternative notions of minimal entailment, as advocated in [10]. The approach can be integrated with systems like DReW [50], that already exploits the mapping by Kr¨ otzsch for OWL 2 EL. Acknowledgement . We thank the anonymous referees for their helpful comments This research has been supported by INDAM - GNCS Project 2016 Ragionamento Defeasible nelle Logiche Descrittive . ## References 1. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proc IJCAI 2005 , pages 364-369, 2005. 2. F. Baader and B. Hollunder. Embedding defaults into terminological knowledge representation formalisms. In Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR'92). Cambridge, MA, October 25-29, 1992. , pages 306-317, 1992. 3. F. Baader and B. Hollunder. Priorities on defaults with prerequisites, and their application in treating specificity in terminological default logic. J. of Automated Reasoning , 15(1):41-68, 1995. 4. J.F. Baget, S. Benferhat, Z. Bouraoui, M. Croitoru, M.L. Mugnier, O. Papini, S. Rocher, and K. Tabia. Inconsistency-tolerant query answering: Rationality properties and computational complexity analysis. In Logics in Artificial Intelligence - 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings , pages 64-80, 2016. 5. C. Beierle, C. Eichhorn, and G. Kern-Isberner. Skeptical inference based on c-representations and its characterization as a constraint satisfaction problem. In Foundations of Information and Knowledge Systems - 9th International Symposium, FoIKS 2016, Linz, Austria, March 7-11, 2016. Proceedings , pages 65-82, 2016. 6. P. A. Bonatti, M. Faella, I. Petrova, and L. Sauro. A new semantics for overriding in description logics. Artif. Intell. , 222:1-48, 2015. 7. P. A. Bonatti, M. Faella, and L. Sauro. Defeasible inclusions in low-complexity dls. J. Artif. Intell. Res. (JAIR) , 42:719-764, 2011. 8. P. A. Bonatti, Carsten Lutz, and Frank Wolter. The Complexity of Circumscription in DLs. J. of Artificial Intelligence Research , 35:717-773, 2009. 9. P. A. Bonatti, I. M. Petrova, and L. Sauro. Optimizing the computation of overriding. In Proc. ISWC 2015 , pages 356-372, 2015. 10. R. Booth, G. Casini, T. Meyer, and I. J. Varzinczak. On the entailment problem for a logic of typicality. In Proc. IJCAI 2015 , pages 2805-2811, 2015. 11. L. Bozzato, T. Eiter, and L. Serafini. Contextualized knowledge repositories with justifiable exceptions. In DL 2014 , volume 1193 of CEUR Workshop Proceedings , pages 112-123. CEUR-WS.org, 2014. 12. K. Britz, J. Heidema, and T. Meyer. Semantic preferential subsumption. In G. Brewka and J. Lang, editors, Proc. KR 2008 , pages 476-484, 2008. 13. G. Casini, T. Meyer, I. J. Varzinczak, , and K. Moodley. Nonmonotonic Reasoning in Description Logics: Rational Closure for the ABox. In Proc. DL 2013 , pages 600-615, 2013. 14. G. Casini and U. Straccia. Rational Closure for Defeasible Description Logics. In Proc. JELIA 2010 , LNAI 6341, pages 77-90. Springer, 2010. 15. G. Casini and U. Straccia. Lexicographic closure for defeasible description logics. In Proc. Australasian Ontology Workshop , pages 28-39, 2012. 16. G. Casini and U. Straccia. Defeasible inheritance-based description logics. Journal of Artificial Intelligence Research (JAIR) , 48:415-473, 2013. 17. G. Deane, K. Broda, and A. Russo. Reasoning in the presence of inconsistency through preferential ALC. In 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015. , pages 67-80, 2015. 18. F. M. Donini, D. Nardi, and R. Rosati. Description logics of minimal knowledge and negation as failure. ACM Transactions on Computational Logic (ToCL) , 3(2):177-225, 2002. 19. T. Eiter and G. Gottlob. On the computational cost of disjunctive logic programming: Propositional case. Annals of Mathematics and Artificial Intelligence , 15(3-4):289-323, 1995. 20. T. Eiter, G. Gottlob, and H. Mannila. Disjunctive datalog. ACM Trans. Database Syst. , 22(3):364-418, 1997. 21. T. Eiter, G. Ianni, T. Lukasiewicz, and R. Schindlauer. Well-founded semantics for description logic programs in the semantic web. ACM Trans. Comput. Log. , 12(2):11, 2011. 22. T. Eiter, G. Ianni, T. Lukasiewicz, R. Schindlauer, and H. Tompits. Combining answer set programming with description logics for the semantic web. Artif. Intell. , 172(12-13):14951539, 2008. 23. M. Gelfond. Handbook of Knowledge Representation, chapter 7, Answer Sets . Elsevier, 2007. 24. M. Gelfond and N. Leone. Logic programming and knowledge representation - the A-Prolog perspective. Artif. Intell. , 138(1-2):3-38, 2002. 25. Oliver Fernandez Gil. On the non-monotonic description logic alc+t min . CoRR , abs/1404.6566, 2014. 26. L. Giordano and V. Gliozzi. Encoding a preferential extension of the description logic SROIQ into SROIQ . In Proc. ISMIS 2015 , volume 9384 of LNCS , pages 248-258. Springer, 2015. 27. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Preferential Description Logics. In Proceedings of LPAR 2007 , volume 4790 of LNAI , pages 257-272. Springer-Verlag, 2007. 28. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. ALC+T: a preferential extension of Description Logics. Fundamenta Informaticae , 96:1-32, 2009. 29. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Prototypical reasoning with low complexity description logics: Preliminary results. In Proc. LPNMR 2009 , pages 430-436, 2009. 30. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Reasoning about typicality in low complexity DLs: the logics EL ⊥ T min and DL-Lite c T min . In Proc. IJCAI 2011 , pages 894-899, Barcelona, 2011. 31. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. A NonMonotonic Description Logic for Reasoning About Typicality. Artificial Intelligence , 195:165-202, 2013. 32. L. Giordano, V. Gliozzi, N. Olivetti, and G. L. Pozzato. Semantic characterization of rational closure: From propositional logic to description logics. Artif. Intell. , 226:1-33, 2015. 33. L. Giordano and D. Theseider Dupr´ e. ASP for minimal entailment in a rational extension of SROEL. TPLP , 16(5-6):738-754, 2016. DOI: 10.1017/S1471068416000399. 34. L. Giordano and D. Theseider Dupr´ e. Reasoning in a Rational Extension of SROEL. In DL2016 , volume 1577 of CEUR Workshop Proceedings , 2016. 35. L. Giordano and D. Theseider Dupr´ e. Reasoning in a rational extension of SROEL. In Proceedings of the 31st Italian Conference on Computational Logic, Milano, Italy, June 20-22, 2016. , volume 1645 of CEUR Workshop Proceedings , pages 53-68. CEUR-WS.org, 2016. 36. V. Gliozzi. A minimal model semantics for rational closure. In G. Kern-Isberner and R. Wassermann, editors, NMR 2016 (16th International Workshop on Non-Monotonic Reasoning) , Cape Town, South Africa, 2016. 37. G. Gottlob, A. Hernich, C. Kupke, and T. Lukasiewicz. Stable model semantics for guarded existential rules and description logics. In Proc. KR 2014 , 2014. 38. P. Ke and U. Sattler. Next Steps for Description Logics of Minimal Knowledge and Negation as Failure. In Proc. DL 2008 , volume 353 of CEUR Workshop Proceedings , 2008. 39. M. Knorr, P. Hitzler, and F. Maier. Reconciling OWL and non-monotonic rules for the semantic web. In ECAI 2012 , page 474479, 2012. 40. S. Kraus, D. Lehmann, and M. Magidor. Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell. , 44(1-2):167-207, 1990. 41. M. Kr¨ otzsch. Efficient inferencing for OWL EL. In Proc. JELIA 2010 , pages 234-246, 2010. 42. M. Kr¨ otzsch. Efficient inferencing for the description logic underlying OWL EL. Tech. Rep. 3005, Institute AIFB, Karlsruhe Institute of Technology , 2010. 43. D. Lehmann and M. Magidor. What does a conditional knowledge base entail? Artificial Intelligence , 55(1):1-60, 1992. 44. D. J. Lehmann. Another perspective on default reasoning. Ann. Math. Artif. Intell. , 15(1):6182, 1995. 45. D. Lembo, M. Lenzerini, R. Rosati, M. Ruzzi, and D.F. Savo. Inconsistency-tolerant query answering in ontology-based data access. J. Web Sem. , 33:3-29, 2015. 46. K. Moodley. Practical Reasoning for Defeasible Description Logics . PhD Thesis, University of Kwazulu-Natal, 2016. 47. Boris Motik and Riccardo Rosati. Reconciling Description Logics and rules. J. ACM , 57(5), 2010. 48. T. C. Przymusinski. Stable semantics for disjunctive programs. New Generation Comput. , 9(3/4):401-424, 1991. 49. U. Straccia. Default inheritance reasoning in hybrid KL-ONE-style logics. In Proc. IJCAI 1993 , pages 676-681, 1993. 50. G. Xiao, T. Eiter, and S. Heymans. The DReW system for nonmonotonic dl-programs. In Proc. CSWS 2012 , pages 383-390, 2012.