In this work we define a rational extension S ROE L(⊓, ×)R T of the low complexity description logic S ROE L(⊓, ×), which underlies the OWL EL ontology language. The logic is extended with 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 a CONP-hard problem while, under rational entailment, instance checking can be computed in polynomial time. In particular, we develop a Datalog materialization calculus for instance checking under rational entailment.
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 [
In this paper we study a preferential extension of the logic SROE L(⊓, ×),
introduced by Kro¨ tzsch [
The semantics of ranked interpretations for DLs was first studied in [
We show that, for general SROE L(⊓, ×)RT KBs, deciding instance checking
under minimal entailment is a CONP-hard problem. Furthermore, we define a Datalog
translation for SROE L(⊓, ×)RT which builds on the materialization calculus in [
A rational extension of SROE L(⊓, ×)
In this section we extend the notion of concept in SROE L(⊓, ×) adding typicality
concepts (we refer to [
C := A | ⊤ | ⊥ | C ⊓ C | ∃R.C | ∃S.Self | {a} where A ∈ NC and R, S ∈ NR. We introduce a notion of extended concept CE as follows:
CE := C | T(C) | CE ⊓ CE | ∃S.CE where C is a SROE L(⊓, ×) concept. Hence, any concept of SROE L(⊓, ×) 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 ⊑ D, where C and D are extended concepts; RBox (as in
[
We define a semantics for SROE L(⊓, ×)RT based on ranked models [
Definition 1. A SROE L(⊓, ×)RT interpretation M is any structure hΔ, <, ·I i where: – Δ is a domain; ·I is an interpretation function that maps each concept name A ∈ NC to a set AI ⊆ Δ, each role name R ∈ NR to a binary relation RI ⊆ Δ × Δ, and each individual name a ∈ NI to an element aI ∈ Δ. ·I is extended to complex concepts as usual: ⊤I = Δ; ⊥I = ∅; {a}I = {aI }; (C ⊓ D)I = CI ∩ DI ; (∃R.C)I = {x ∈ Δ | ∃y ∈ CI : (x, y) ∈ RI }; (∃R.Self )I = {x ∈ Δ | (x, x) ∈ RI }; and the composition of role interpretations is defined as follows:
R1I ◦ R2I = {(x, z) | (x, y) ∈ R1I and (y, z) ∈ R2I, for some y ∈ Δ} – < is an irreflexive, transitive, well-founded and modular relation over Δ; – the interpretation of concept T(C) is defined as follows:
(T(C))I = M in<(CI ) where M in<(S) = {u : u ∈ S and ∄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 ∈ M in<(S) or ∃y ∈ M in<(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., CI 6= ∅ implies (T(C))I 6= ∅).
In the following, we will refer to SROE L(⊓, ×)RT interpretations as ranked
interpretations. Indeed, as in [
Observe that semantics of the typicality operator defined above is exactly the same
as the one introduced in [
Definition 2 (Satisfiability and rational entailment). An interpretation M = hΔ, < , ·I i satisfies: • a concept inclusion C ⊑ D if CI ⊆ DI ; • a role inclusion S ⊑ T if SI ⊆ T I ; • a generalized role inclusion R ◦ S ⊑ T if RI ◦ SI ⊆ T I • a role conjunction S1 ⊓ S2 ⊑ T if S1I ∩ S2I ⊆ T I ; • a concept product axiom C × D ⊑ T if CI × DI ⊆ T I ; • a concept product axiom R ⊑ C × D if RI ⊆ CI × DI ; • an assertion C(a) if aI ∈ CI ; • an assertion R(a, b) if (aI , bI ) ∈ RI .
Given a KB K = (TBox , RBox , ABox ), an interpretation M =hΔ, <, ·I 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 = hΔ, <, ·I 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 ⊑ 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 =hΔ, <, ·I 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, corresponding to Lehmann and Magidor’s postulates of rational
consequence relation [
if (T(A) ⊓ B )I 6= ∅, then (T(A ⊓ B ))I ⊆ (T(A))I
and, in this form, it is a rephrasing of property (fT − R), in the semantics with selection
function of the operator T studied in [
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, and Paul is a typical young student. Example 1. TBox : (a) T(Italian ) ⊑ ∃hasHair .{Black } (b) T(Student ) ⊑ Young (c) T(Student ) ⊑ MathHater (d) T(Student ⊓ Nerd ) ⊑ MathLover (e) ∃hasHair .{Black } ⊓ ∃hasHair .{Blond } ⊑ ⊥ (f ) MathLover ⊓ MathHater ⊑ ⊥ (g) ∃friendOf .{mary } ⊑ T(Student ) ABox : Student (mary ), friendOf (mario, mary), (Student ⊓ Italian )(mario), T(Student ⊓Italian )(luigi), T(Student ⊓Young)(paul), T(Student ⊓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 ⊓ Worker ) ⊑ 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: ⊤ ⊑ ∃U.T(Student ⊓ Italian ), where U is the universal role (⊤ × ⊤ ⊑ U ).
Standard DL inferences hold for T(C) concepts and T(C) ⊑ 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 rational monotonicity (RM) and by cautious monotonicity (CM). Instead, as Tom is a typical nerd student, and typical nerd student 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 SROE L(⊓, ×)RT knowledge bases can be defined. A KB in SROE L(⊓, ×)RT is in normal form if it admits all the axioms of a SROE L(⊓, ×) KB in normal form:
C(a) R(a, b) A ⊑ ⊥ ⊤ ⊑ C A ⊑ {c}
A ⊑ C A ⊓ B ⊑ C ∃R.A ⊑ C A ⊑ ∃R.B
{a} ⊑ C ∃R.Self ⊑ C A ⊑ ∃R.Self R ⊑ T
R ◦ S ⊑ T
R ⊓ S ⊑ T
A × B ⊑ R
R ⊑ C × D
(where A, B, C, D ∈ NC , R, S, T ∈ NR and a, b, c ∈ NI ) and, in addition, it admits
axioms of the form: A ⊑ T (B) and T (B) ⊑ C with A, B, C ∈ NC . Extending the
results in [
XC ⊑ T(YC ), T(YC ) ⊑ XC , YC ⊑ C, C ⊑ YC
Then the new KB undergoes the normal form transformation for SROE L(⊓, ×) [
Example 2. Considering again the TBox in Example 1, inclusion (a) T(Italian ) ⊑ ∃hasHair .{Black } is transformed in the following set of inclusions: (a1) XI ⊑ ∃hasHair .{Black } (a2) XI ⊑ T(Italian ) (a3) T(Italian ) ⊑ XI Inclusion (d) T(Student ⊓ Nerd ) ⊑ MathLover is mapped to the set of inclusions: (d1) XSN ⊑ MathLover (d2) XSN ⊑ T(YSN ) (d3) T(YSN ) ⊑ XSN (d4) Student ⊓ Nerd ⊑ YSN (d5) YSN ⊑ Student ⊓ Nerd Then (a1) is transformed further (the normal form transformation for SROE L(⊓, ×)) into: (a′1) XI ⊑ ∃hasHair .B (a′1′) B ⊑ {Black}
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 ⊓ Nerd )(tom) becomes XSN (tom), where XSN 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 that Luigi has black hair) using rational monotonicity, as we do not know whether there is some typical Italian who is young. To supports 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′ =hΔ, <, Ii is preferred to M′ = hΔ′, <′, I′i (M ≺ M′) if: Δ = Δ′; CI = CI for all non-extended concepts C; for all x ∈ Δ, kM(x) ≤ kM′ (x), and there exists y ∈ Δ such that kM(y) < kM′ (y).
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 ⊓ Italian) ⊑ ∃hasHair .{Black } is satisfied, as nothing prevents a Young ⊓ Italian individual from having rank 0.
In particular, we consider the notion of minimal canonical model defined in [
Among canonical models, we select the minimal ones.
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 |=min F if, for all minimal canonical models M of K, M satisfies F .
We can show that the problem of instance checking in SROE L(⊓, ×)RT under
minimal entailment is CONP-hard. The proof is based on a reduction from tautology
checking of propositional 3DNF formulae to instance checking in SROE L(⊓, ×)RT
and its structure has similarities with the proof of CO-NP-hardness for F L subsumption
in [
Theorem 1. Instance checking in SROE L(⊓, ×)RT under minimal entailment is CONPhard.
Proof. (sketch) Given an alphabet of propositional variables L = {p1, . . . , pk} and a propositional formula in 3DNF γ = G1 ∨ . . . ∨ Gn as defined above, we define a KB K = (TBox , RBox , ABox ) in SROE L(⊓, ×)RT as follows. We introduce in NC two concept names Ph, P h for each variable ph ∈ L, a concept name Dγ associated with the formula γ and a new concept name E. Let R ∈ NR be a role name and a ∈ NI be an individual name. We define K as follows: RBox = {Ph × P h ⊑ R, h = 1 , ..., k }, ABox = {T(Ph ⊓ P h)(a), h = 1, ..., k} ∪ {T(E)(a)}, and TBox contains the following inclusions: (1) T(Ph) ⊓ T(P h) ⊑ ⊥, (2) T(⊤) ⊓ ∃R.T(⊤) ⊑ ⊥ (3) T(E) ⊓ Ci1 ⊓ Ci2 ⊓ Ci3 ⊑ Dγ ,
for each Gi = li1 ∧ li2 ∧ li3 where h = 1, . . . , k and, for each i = 1, . . . , n and j ∈ {1, 2, 3}, Cij is defined as follows:
Cij =
T(Ph) ∃U.(T(⊤) ⊓ T(Ph)) if lij = ph if lij = ¬ph Let us consider any model M= hΔ, <, ·I i of K . Observe that, as aI ∈ Ph ⊓ P h, aI cannot have rank 0, otherwise it would be both a typical Ph and a typical P h, falsifying (1). By the role inclusions each Ph element is in relation R with any P h element. Also, by (2), there cannot be a Ph element x and a P h element y both with rank 0, otherwise x and y would be related by R and axiom (2) excludes that two T(⊤) elements are in relation R. It is possible that, in a model of K , there are no Ph elements with rank 0 and no P h elements with rank 0. However, if we consider minimal canonical models of K , there must be either a Ph element or a P h element with rank 0.
Remember that kM(C) is the rank of a concept C in a ranked model M. It can be seen that, in all the minimal canonical models of K , for all h = 1, . . . , k, the following conditions hold: (i) either kM(Ph) = 0 or kM(P h) = 0; (ii) kM(Ph ⊓ P h) = 1 and kM(aI ) = 1.
As a consequence, aI is either a typical Ph element (when the rank of P h is 0) or a typical P h (when the rank of Ph is 0). So there are alternative minimal canonical models in which, for each h, aI is either a T(Ph), and in this case there exists a typical P h element with rank 0; or a is a T(P h), and in this case there exists a typical Ph element with rank 0. Therefore, in any minimal canonical models M of K : either aI ∈ (T(Ph))I or aI ∈ (∃U .(T(⊤) ⊓ T(Ph )))I (but not both). Then for aI the two concepts in the definition of Cij are disjoint and complementary and the following can be proved:
K |=min Dγ (a) if and only if γ is a tautology ⊓⊔
It is an open issue whether a similar proof can be done also for simple knowledge
bases (i.e., for SROE L(⊓, ×)RT knowledge bases where the typicality operator only
occurs on the left hand side of concept inclusions T(C) ⊑ D). For simple KBs, it was
proved for ALC + TR [
Note that K , in the proof above, has alternative minimal canonical models with
incomparable rank assignments. The existence of alternative minimal models for a KB
with free occurrences of typicality in the propositional case was observed in [
Deciding rational entailment in polynomial time
While instance checking in SROE L(⊓, ×)RT under minimal entailment is
CONPhard, 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 SROE L(⊓, ×),
proposed by Kro¨ tzsch [
The calculus in [
Besides the constants for individuals in NI (which are assumed to be finitely many),
the calculus in [
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 SROE L(⊓, ×)RT, i.e. for querying whetherK |=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 [
A query Q of the form T(C)(a), or C(a), is mapped to a goal GQ 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
new concept name, by adding C ⊑ A to the TBox [
We define Π(K) in such a way that GQ is derivable in Datalog from Π(K) (written Π(K) ⊢ GQ) if and only if K |=sroelrt Q .
ΠK includes the result of the input translation in section 3 in [
A ⊑ C; – subEx (R, A, C ) is used for ∃R.A ⊑ C ; and similar statements represent other axioms in the normalized KB.
The following is the additional mapping for the extended syntax of the SROEL(⊓, ×)RT normal form (note that no mapping is needed for assertions T(C)(a), as they do not occur in a normalized KB):
A ⊑ T(B ) 7→ supTyp(A, B )
T(B ) ⊑ C 7→ subTyp(B , C ) Also, we need to add top(⊤) to the input specification.
ΠIR contains all the inference rules from [
Note that “statements inst(a, b), with a and b individuals, encode equality of a and b”
[
ΠRT , i.e. the set of rules to deal with typicality, is as follows; it contains rules for supTyp and subTyp axioms, and rules that deal with the rank of domain elements. In the rules, x, y, z, A, B, C are all Datalog variables. (SupTyp) typ(x , z ) ← supTyp(y, z ), inst (x , y) (SubTyp) inst (x , z ) ← subTyp(y, z ), typ(x , y) (Refl ) inst (x , y) ← typ(x , y) (A0 ) typ(auxC , C ) ← inst (x , C ) (A1 ) leqRank (x , y) ← typ(x , B ), inst (y, B ) (A2 ) sameRank (x , y) ← typ(x , A), typ(y, A) (A3 ) typ(x , B ) ← sameRank (x , y), inst (x , B ), typ(y, B ) (A4 ) typ(x , B ) ← inst (x , A), supTyp(A, B ) (B1 ) sameRank (x , z ) ← sameRank (x , y), sameRank (y, z ) (B2 ) sameRank (x , y) ← sameRank (y, x ) (B3 ) sameRank (x , x ) ← inst (x , T ) (B4 ) leqRank (x , y) ← sameRank (y, x ) (B5 ) leqRank (x , z ) ← leqRank (x , y), leqRank (y, z ) (B6 ) sameRank (x , y) ← leqRank (x , y), leqRank (y, x ) (B7 ) sameRank (x , y) ← nom(y), inst (x , y) Rule (Refl ) corresponds to the reflexivity property (see Section 2). Rules (A0 ) − (A4 ) 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 ); if x is an A element and all A’s are typical B’s, then x is a typical A (A4 ). (B1 ) − (B7 ) define properties of rank order. In particular, by (B7 ), two constants that correspond to the same domain element have the same rank.
The semantic properties of rational consequence relation introduced in Section 2 are enforced by the specification above. Consider, for instance, (CM ). Suppose that subTyp(A, B ) and subTyp(A, C ) are in ΠK (as T(A) ⊑ B , T(A) ⊑ C are in K) and that D is a concept name defined to be equivalent to A ⊓ B in K. Suppose that typ(a, D ) holds. One can infer typ(a, A) and hence inst (a, C ), i.e., typical A ⊓ B’s inherit from typical A’s the property of being C’s (the inference for P aul 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 auxA (who is a typical A, by (A1 ), and a D, since all the typical A’s are also B’s and hence A ⊓ B’s) have the same rank. In fact, using(A1 ) twice, one can conclude both leqRank (a, auxA) and leqRank (auxA, a) so that, by (B6 ), sameRank (a, auxA). 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 also the properties (RM ) and (LLE ) are enforced by the rules above. In particular, for (RM), we can show that: from the fact that there is a domain element a who 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 who is a typical A ⊓ C element (i.e. that typ(b, D ) holds, for some concept D equivalent to A ⊓ C), we can conclude that b is also a typical A element (i.e. typ(b, A) holds). Inference in SROE L(⊓, ×) already takes care of the semantic properties of conjunctive consequences (And ) and right weakening (RW ).
Theorem 2. For a SROE L(⊓, ×)RT 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) ⊢ GQ.
Proof. (sketch) For completeness, we procede by contraposition, similarly to [
Proving the soundness of the Datalog encoding, requires showing that, if Π(K) ⊢
GQ, 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 [
The following statements: - if Π(K) ⊢ inst (c, A), for A ∈ NC , then K |=sroelrt κ(c) ⊑ A; - if Π(K) ⊢ inst (c, d ), for d ∈ NI , then K |=sroelrt κ(c) ⊑ {d}; - if Π(K) ⊢ typ(a, A), then K |=sroelrt κ(c) ⊑ T(A); - if Π(K) ⊢ triple(c, R, d ), then K |=sroelrt κ(c) ⊑ ∃R.κ(d); - if Π(K) ⊢ self (c, R), for A ∈ NC , then K |=sroelrt κ(c) ⊑ ∃R.Self ; - if Π(K) ⊢ sameRank (c, d ) then for all models M of K, kM(cI ) = kM(dI ); - if Π(K) ⊢ leqRank (c, d ) then, for all models M of K, kM(cI ) ≤ kM(dI ). can be proved by induction on the height of the derivation tree of each atom from the program Π(K). ⊓⊔ Π(K) contains a polynomial number of rules and exploits a polynomial number of concepts in the size of K, hence instance checking in SROE L(⊓, ×)RT 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 [
For simple SROE L(⊓, ×)RT knowledge bases, i.e., for KBs where the
typicality operator only occurs on the left hand side of inclusions, the materialization
calculus for subsumption can be used to construct the rational closure of TBox, adopting
the construction in [
The correspondence between the rational closure construction and the canonical
minimal model semantics in [
Related Work
Among the recent nonmonotonic extensions of DLs are the formalisms for combining
DLs with logic programming rules, such as for instance, [
Preferential extensions of low complexity DLs in the E L and DL-lite families have
been studied In [
Conclusions
In this paper we defined a rational extension SROE L(⊓, ×)R T of the low
complexity description logic SROE L(⊓, ×), which underlies the OWL EL ontology language,
introducing a typicality operator. For general KBs, we have shown that minimal
entailment in SROE L(⊓, ×)RT is CONP-hard. When free occurrences of typicality
concepts in concept inclusions are allowed, alternative minimal models may exist with
different rank assignments to concepts. In [
Building on the materialization calculus for SROE L(⊓, ×) in Datalog presented
in [
This result also provides a polynomial upper bound for the construction of the
rational closure of a knowledge base in SROE L(⊓, ×)RT. Although for the fragment of
SROE L(⊓, ×)RT which is also included in the language of ALC + TR in [
Future work may also include optimizations, based on modularity as in [
tablished. A further issue to understand is whether a materialization calculus can be
defined also for the preferential extensions of DLs in the E L family in [
Apart from providing a complexity upper bound, the Datalog encoding presented
in this paper is intended to provide a way to integrate the use of SROE L(⊓, ×) KBs
under rational entailment with other kinds of reasoning that can be performed in ASP,
and, by extending the encoding to deal with alternative models of the KB, also to allow
the experimentation of alternative notions of minimal entailment, as advocated in [
Acknowledgement. This research has been supported by INDAM - GNCS Project 2016 Ragionamento Defeasible nelle Logiche Descrittive.