SWC OWL Proofs

Embedding RDFS Entailment

Theorem A RIF-RDFS-satisfiable list-free RIF-RDF combination C=<R,{S₁,...,S_n}> RIF-RDFS-entails a generalized RDF graph T if and only if merge({R, R^RDFS, tr_R(S₁), ..., tr_R(S_n)}) entails tr_Q(T); C RIF-RDFS-entails a condition formula φ if and only if merge({R, R^RDFS, tr_R(S₁), ..., tr_R(S_n)}) entails φ.

Proof.

In the proof we abbreviate merge({R, R^RDFS, tr_R(S₁), ..., tr_R(S_n)}) with R'.

The proof is then obtained from the proof of correspondence for RDF entailment in the previous section with the following modifications: (*) in the (=>) direction we need to slightly amend the definition of I to account for rdfs:Literal and rdfs:Resource, and show that I is an RDFS-interpretation and (**) in the (<=) direction we need to show that I' is a model of R^RDFS.

(*) In addition to the earlier assumptions about I, we assume that tr("s"^^rdf:XMLLiteral)[rdf:type -> rdfs:Literal] is not satisfied in I, for any typed literal of the form (s, rdf:XMLLiteral) in V_TL.

We amend the definition of I by changing the definitions of LV and IEXT to the following:

• LV is (union of the value spaces of all considered datatypes) union (set of all k in D_ind such that I_truth(I_frame(k)(I_C(rdf:type),I_C(rdfs:Literal)))=t).

Clearly, this change does not affect satisfaction of the RDF axiomatic triples and the semantic conditions 1 and 2. To see that condition 3 is still satisfied, consider some non-well-typed XML literal t. By assumption, tr(t)[rdf:type -> rdfs:Literal] is not satisfied and thus IL(t) is not in ICEXT(rdfs:Literal). And, since IL(t) is not in the value space of any considered datatype, it is not in LV.

• For every k, a, and b ∈ D_ind such that k≠I_C(rdf:type) or b≠I_C(rdfs:Resource), (a, b) ∈ IEXT(k) iff I_truth(I_frame(a)(k,b))=t;
• for every a ∈ D_ind, (a, I_C(rdfs:Resource)) ∈ IEXT(I_C(rdf:type)).

Clearly, this change does not affect satisfaction of the RDF axiomatic triples and semantic conditions, nor does it affect satisfaction of the graphs S₁,...,S_n. It also does not affect satisfaction of the entailed graph or condition, since (by assumption) this does not contain a mention of rdfs:Resource.

To show that I is an RDFS-interpretation, we need to show that I satisfies the RDFS axiomatic triples and the RDFS semantic conditions.

Satisfaction of the axiomatic triples follows immediately from the inclusion of tr(t) in R^RDFS for every RDFS finite-axiomatic triple t, the fact that I is a model of R^RDFS, construction of I, and the extension of I in the proof of the RDF entailment embedding. Consider the RDFS semantic conditions:

1	(a) x is in ICEXT(y) if and only if <x,y> is in IEXT(I(rdf:type)) (b) IC = ICEXT(I(rdfs:Class)) (c) IR = ICEXT(I(rdfs:Resource)) (d) LV = ICEXT(I(rdfs:Literal))
2	If <x,y> is in IEXT(I(rdfs:domain)) and <u,v> is in IEXT(x) then u is in ICEXT(y)
3	If <x,y> is in IEXT(I(rdfs:range)) and <u,v> is in IEXT(x) then v is in ICEXT(y)
4	IEXT(I(rdfs:subPropertyOf)) is transitive and reflexive on IP
5	If <x,y> is in IEXT(I(rdfs:subPropertyOf)) then x and y are in IP and IEXT(x) is a subset of IEXT(y)
6	If x is in IC then <x, I(rdfs:Resource)> is in IEXT(I(rdfs:subClassOf))
7	If <x,y> is in IEXT(I(rdfs:subClassOf)) then x and y are in IC and ICEXT(x) is a subset of ICEXT(y)
8	IEXT(I(rdfs:subClassOf)) is transitive and reflexive on IC
9	If x is in ICEXT(I(rdfs:ContainerMembershipProperty)) then: < x, I(rdfs:member)> is in IEXT(I(rdfs:subPropertyOf))
10	If x is in ICEXT(I(rdfs:Datatype)) then <x, I(rdfs:Literal)> is in IEXT(I(rdfs:subClassOf))

Conditions 1a and 1b are simply definitions of ICEXT and IC, respectively. By definition it is the case that every element k in D_ind is in ICEXT(I(rdfs:Resource)). Since IR=D_ind, it follows that IR = ICEXT(I(rdfs:Resource)), establishing 1c. Clearly, every object in ICEXT(I(rdfs:Literal)) is in LV, by definition. Consider any value k in LV. By definition, either k is in the value space of some considered datatype or I_truth(I_frame(k)(I_C(rdf:type),I_C(rdfs:Literal)))=t. In the latter case, clearly k is in ICEXT(I(rdfs:Literal)). In the former case, k is in the value space of some datatype with some label D, and thus I_truth(I_F(I_C(pred:isD))(k))=t. By the last rule in R^RDFS, it must consequently be the case that I_truth(I_frame(k)(I_C(rdf:type),I_C(rdfs:Literal)))=t, and thus k is in ICEXT(I(rdfs:Literal)). This establishes satisfaction of condition 1d in I.

Satisfaction in I of conditions 2 through 10 follows immediately from satisfaction in I of the 2nd through the 12th rule in the definition of R^RDFS.

This establishes the fact that I is an RDFS-interpretation.

(**) Consider R^RDFS. Satisfaction of R^RDF was established in the proof in the previous section. Satisfaction of the facts corresponding to the RDFS axiomatic triples in I' follows immediately from the definition of common-RIF-RDF-interpretation and the fact that I is an RDFS-interpretation, and thus satisfies all RDFS axiomatic triples.

Satisfaction of the 1st through the 12th rule in R^RDFS follow straightforwardly from the RDFS semantic conditions 1 through 10. Satisfaction of the 13th rule follows from the fact that, given an ill-typed XML literal t, IL(t) is not in LV (by RDF semantic condition 3), ICEXT(rdfs:Literal)=LV, and the fact that the ex:illxml predicate is only true for ill-typed XML literals. Finally, satisfaction of the last rule in R^RDFS follows from the fact that ICEXT(rdfs:Literal)=LV, the definition of LV as a superset of the union of the value spaces of all datatypes, and the definition of the pred:isD predicates. This establishes the fact that I' is a model of R^RDFS.   ☐

Theorem A list-free RIF-RDF combination <R,{S₁,...,S_n}> is RIF-RDFS-satisfiable if and only if merge({R, R^RDFS, tr_R(S₁), ..., tr_R(S_n)}) does not entail rif:error.

Proof. The theorem follows immediately from the previous theorem and the observations in the proof of the second theorem in the previous section.   ☐

DL-Document embedding lemma

RIF-BLD DL-document formula Lemma A RIF-BLD DL-document formula R dl-entails a DL-condition φ if and only if tr(R) entails tr(φ).

Proof. We prove both directions by contraposition.

(=>) Assume tr(R) does not entail tr(φ). This means there is some semantic multi-structure Î that is a model of tr(R'), but I = <TV, DTS, D, D_ind, D_func, I_C, I_V, I_F, I_frame, I_NF, I_sub, I_isa, I₌, I_external, I_truth> is not a model of tr(φ).
Consider the dl-semantic multi-structure Î*, which is obtained from Î as follows: I* = <TV, DTS, D, D_ind, D_func, I*_C, I*_C', I_V, I_F, I*_frame, I_NF, I*_sub, I*_isa, I₌, I_external, I_truth>, with I*_C', I*_frame, I*_sub, and I*_isa defined as follows: Let t be an element in D such that I_truth(t)=t and let f in D be such that I_truth(f)=f.

• for every constant c, with c'=tr'(c), I*_C'(c)=I_C(c');
• for every constant c' used as unary predicate symbol in tr(R) or tr(φ) such that c'=tr'(c) for some constant c, and every object k in D_ind, I_truth(I_F(I_C(c'))(k))=t iff I*_frame(k)((I_C'(rdf:type), I_C'(c))=t;
• for every constant b' used as binary predicate symbol in tr(R) or tr(φ) such that b'=tr'(b) for some constant b, and every pair (k, l) in D_ind × D_ind, I_truth(I_F(I_C(b'))(k,l))=t iff I*_frame(k)((I_C'(b),l))=t,
• if I*_frame(k)((b₁,...,b_n))=t and I*_frame(k)((c₁,...,c_m))=t for any two finite bags (b₁,...,b_n) and (c₁,...,c_m), then I*_frame(k)((b₁,...,b_n,c₁,...,c_m))=t;
• I*_frame(b)=f for any other bag b;
• for any two k, l ∈ D, I*_sub(k,l)=t if for every u ∈ D, I_truth(I_F(k)(u))=t implies I_truth(I_F(l)(u))=t, otherwise I*_sub(k,l)=f;
• for any two k, l ∈ D, I*_isa(k,l)=t if I_truth(I_F(k)(u))=t, otherwise I*_isa(k,l)=f.

Observe that tr(R) and tr(φ) do not include frame formulas.
To show that Î* is a model of R and I* is not a model of φ, we only need to show that (+) for any frame formula a[b -> c] that is a DL-condition, I* is a model of a[b -> c] iff I is a model of tr(a[b -> c]). This argument straightforwardly extends to the case of frames with multiple b_is and c_is, since in RIF semantic structures the following condition is required to hold: TVal_I(a[b₁->c₁ ... b_n->c_n]) = t if and only if TVal_I(a[b₁->c₁]) = ... = TVal_I(a[b_n->c_n]) = t [RIF-BLD]. The argument for formulas a # b and a ## b is analogous.

Consider the case b=rdf:type. Then,
I* is a model of a[b -> c] iff I_truth(I*_frame(I(a))(I_C'(rdf:type),I_C'(c)))=t.
From the definition of I* we obtain
I_truth(I*_frame(I(a))(I_C'(rdf:type),I_C'(c)))=t iff I*_frame(I(a))(I_C'(rdf:type),I_C'(c))=t.
By definition of the embedding, we know that tr'(c) is used as unary predicate symbol in tr(R) or tr(φ). From the definition of I* we obtain
I*_frame(I(a))(I_C'(rdf:type),I_C'(c))=t iff I_truth(I_F(I_C(tr'(c)))(I(a)))=t.
Finally, since tr(a[b -> c])=tr'(c)(a), we obtain
I_truth(I_F(I_C(tr'(c)))(I(a)))=t iff I is a model of tr(a[b -> c]).
From this chain of equivalences follows that I* is a model of a[b -> c] iff I is a model of tr(a[b -> c]).

The argument for the case b≠rdf:type is analogous, thereby obtaining (+).

(<=) Assume R does not dl-entail φ. This means there is some dl-semantic multi-structure Î that is a model of R, but I = <TV, DTS, D, D_ind, D_func, I_C, I_C', I_V, I_F, I_frame, I_NF, I_sub, I_isa, I₌, I_external, I_truth>, is not a model of φ. Let B be the set of constant symbols occurring in the frame formulas of the forms a[rdf:type -> b] and a[b -> c] in R or φ.
Consider the semantic multi-structure Î*, which is obtained from Î as follows: I* = <TV, DTS, D, D_ind, D_func, I*_C, I_V, I*_F, I*_frame, I_NF, I_sub, I_isa, I₌, I_external, I_truth>. Let t and f in D be such that I_truth(t)=t and I_truth(f)=f. We define I*_C, I*_frame, and I*_F as follows:

• I*_C(tr'(c))=I_C'(c) and I*_C(c)=I_C(c), for any constant c not in the range of tr';
• I*_frame(b)=f for any finite bag b of D, and
• I*_F is defined as follows:
  • for every constant c, given an object k in D_ind, if I_truth(I_frame(k)((I_C'(rdf:type), I_C'(c)))=t, I*_F(I*_C(tr'(c)))(k)=t; I*_F(I*_C(tr'(c)))(k')=f for any other k' in D_ind,
  • for every constant c, given a pair (k, l) in D_ind × D_ind, if I_truth(I_frame(k)((I_C'(c),l)))=t, I*_F(tr'(c))(k,l)=t;I*_F(tr'(c))(k',l')=f for any other pair (k', l') in D_ind × D_ind, and
  • I*_F(c)=I_F(c) for every other constant c.

Observe that R and φ do not include predicate formulas involving derived constant symbols tr'(c). The remainder of the proof is analogous to the (=>) direction.   ☐

Normalization Lemma

Normalization Lemma Given a combination C=<R,{O₁,...,O_n}>, where O₁,...,O_n are simplified OWL 2 RL ontologies that do not import ontologies, C RIF-OWL Direct-entails φ iff C'=<R,{tr_N(O₁),...,tr_N(O_n)}> RIF-OWL Direct-entails φ.

Proof. We prove both directions by contradiction: if the entailment does not hold on the one side, we show that it also does not hold on the other.

(=>) Assume C' does not RIF-OWL Direct-entail φ. This means there is a common-RIF-OWL Direct-interpretation (Î, I) that is a model of C', but I is not a model of φ.

By the definition of satisfaction of axioms and assertions in Section 2.3 and the interpretation of object property, data range, and class expressions in Section 2.2 in [OWL2-Semantics] it is easy to verify that, if for every axiom d appearing in {O₁,...,O_n}, I satisfies tr_N(d), then I satisfies O₁,..., and O_n, and thus (I, I) satisfies C. Since I is not a model of φ, C does not RIF-OWL Direct-entail φ.

(<=) Assume C does not RIF-OWL Direct-entail φ. This means there is a common-RIF-OWL Direct-interpretation (Î, I) that is a model of C, but I is not a model of φ. It is easy to verify, by the definition of satisfaction of axioms and assertions in Section 2.3 and the interpretation of object property, data range, and class expressions in Section 2.2 in [OWL2-Semantics], that I satisfies tr_N(O₁),..., and tr_N(O_n). So, (Î, I) is a model of C', and thus C' does not RIF-OWL Direct-entail φ.

  ☐

Combination Embedding Lemma

Normalized Combination Embedding Lemma Given a datatype map D conforming with T, a RIF-OWL DL-combination C=<R,{O₁,...,O_n}>, where {O₁,...,O_n} is an imports-closed set of normalized OWL 2 RL ontologies with vocabulary V, OWL Direct-entails a DL-condition φ with respect to D iff merge({R', R^OWL-Direct(V), tr_O(O₁), ..., tr_O(O_n)}) dl-entails φ, where R' is like R, except that every subformula of the form a#b has been replaced with a[rdf:type -> b].

Proof.

We prove both directions by contraposition.

In the proof we abbreviate merge({R', R^OWL-Direct(V), tr_O(O₁), ..., tr_O(O_n)} with R*.

(=>) Assume R* does not dl-entail φ. This means there is a dl-semantic multi-structure Î that is a model of R* but I = <TV, DTS, D, D_ind, D_func, I_C, I_C', I_V, I_F, I_frame, I_NF, I_sub, I_isa, I₌, I_external, I_truth> is not a model of φ.

We call a structure I named for R* if for every object k ∈ D_ind that is not in the value space of some datatype in DTS, k=I_C(c), where c is either an IRI identifying an individual in V or a constant appearing as an individual in R. This definition extends naturally to dl-semantic multi-structures.

We now show that there is a named dl-semantic multi-structure Î' that is a model of R* such that I' is not a model of φ.

The set of unnamed individuals in I is the set of objects k ∈ D_ind that are not in the value space of some datatype in DTS, and there is no IRI c identifying an individual in V or constant c appearing as an individual in R such that k=I_C(c).

Let Î' be obtained from Î by removing all unnamed individuals from D_ind and removing the corresponding tuples in the domains and ranges of the various mapping functions in the structures in Î. Clearly, I' is not a model of φ: condition formulas do not contain negation, and so every condition formula that is satisfied by I' is also satisfied by I.

Consider any rule r in R*. If r is a variable-free rule implication or atomic formulas it is clearly satisfied Î', by satisfaction of r in Î are construction of Î'. A universal fact can be seen as a rule with the empty condition And(). Let r be a rule with a condition ψ that is satisfied by I'. Since ψ does not contain negation, ψ is also satisfied by I. Now, if every variable in the conclusion of r appears also in the condition ψ, every variable is mapped to a named individual, and thus the conclusion is satisfied by satisfaction in I and construction of I'. Now, if there is a variable ?x in the conclusion that does not appear in ψ, I satisfies the conclusion for every assignment of ?x to any element in D_ind. Since the individual domain of I' is a strict subset of D_ind, the conclusion is also satisfied in I'. Therefore, Î' is a model of R*. In the remainder we assume Î=Î'.

We define CExt(c)={u | u ∈ D_ind and I_truth(I_frame(u)(rdf:type, I_C(c)))} as the class extension of the constant c. Furthermore, we define D_D=(union of the value spaces of all datatypes in D).

Consider the pair (Î*,I), where Î* is obtained from Î as follows: I* = <TV, DTS, D*, D*_ind, D_func, I*_C, I_C', I_V, I_F, I*_frame, I_NF, I_sub, I_isa, I₌, I_external, I_truth>, where t, f ∈ D* such that I_truth(t)=t and I*_truth(f)=f, and

• D*_ind=D_ind union (union of the value spaces of all datatypes in D);
• D*=D union D*_ind;
• I*_C is like I_C except that it maps all constants with symbol spaces in D\DTS to the values in the in the corresponding datatypes, according to the respective lexical-to-value mappings;
• I*_frame is defined as follows:
  • I*_frame(k)(I_C'(rdf:type),I_C'(rdfs:Literal))=t if k ∈ D_D, otherwise I*_frame(k)(I_C'(rdf:type),I_C'(rdfs:Literal))=f,
  • otherwise I*_frame is like I_frame;

and I=< IR, LV, C, OP, DP, I, DT, LT, FA > is a tuple defined as follows:

• LV=D_D,
• IR=D_ind\LV,
• DT(rdfs:Literal)=LV,
• DT(d') = the value space of D(d'), if d' is a datatype identifier in V in the domain of D,
• DT(d') = set of all objects k such that I_truth(I_frame(k)(I_C'(rdf:type),I_C'(<c>))) = t, for every datatype identifier d' in V, not in the domain of D,
• C(c) = set of all objects k such that I_truth(I_frame(k)(I_C'(rdf:type),I_C'(<c>))) = t, for every class identifier in V,
• OP(p) = set of all pairs (k, l) such that I_truth(I_frame(k)( I_C'(<p>), l ))) = t (true), for every object property identifier p in V and not in {owl:topObjectProperty,owl:bottomObjectProperty};
• OP(owl:topObjectProperty) = IR × IR;
• OP(owl:bottomObjectProperty) = { };
• DP(p) = set of all pairs (k, l) such that I_truth(I_frame(k)( I_C'(<p>), l ))) = t (true), for every datatype property identifier p in V and not in {owl:topDataProperty,owl:bottomDataProperty};
• OP(owl:topDataProperty) = IR × LV;
• OP(owl:bottomDataProperty) = { };
• LT((s, d)) = I_C("s"^^d) for every well-typed literal (s, d) in V;
• I(i) = I_C(<i>) for every IRI i identifying an individual in V;
• FA is the empty mapping.

When referring to rules in the remainder we mean rules in R^OWL-Direct(V,R), unless otherwise specified.

We have that I* has a separation between the object and data domains: (+) each object is either in CExt(owl:Thing) or in CExt(rdfs:Literal) and D_D: each non-data value in D_ind is in CExt(owl:Thing) by rule (vii) and the fact that I* is a named structure, and each data value is in CExt(rdfs:Literal) by construction of I*. The two sets are distinct by satisfaction of rule (ii) in I.

It is straightforward to see that Î* is a model of R* and I* is not a model of φ.

According to its definition, an OWL2 direct interpretation with respect to a datatype map D must fulfill the following conditions, where L(d) denotes the lexical space, V(d) denotes the value space and L2V(d) denotes to lexical-to-value mapping of a datatype d:

1. IR is a nonempty set,
2. LV is a nonempty set disjoint with IR and including the value spaces of all datatypes in D,
3. C : V_C → 2^IR
4. DT : V_D → 2^LV, where DT is the same as in D for each datatype d
5. OP : V_IP → 2^IR×IR
6. DP : V_DP → 2^IR×LV
7. LT  : TL → LV, where TL is the set of typed literals in V_L and LT((s,d))=L2V(d)(s), for every typed literal (s,d) ∈ V_L
8. I  : V_I → IR
9. C(owl:Thing) = IR
10. C(owl:Nothing) = { }
11. OP(owl:topObjectProperty) = IR × IR
12. DP(owl:topDataProperty) = IR × LV
13. OP(owl:bottomObjectProperty) = { }
14. DP(owl:bottomDataProperty) = { }
15. DT(rdfs:Literal) = LV

Condition 1 is met because D_ind is a nonempty set. Clearly LV disjoint with IR and contains the value space for each datatype in D; therefore, condition 2 is met. Conditions 3 through 9 and 11 through 15 are met by the definitions of I* and I, and the property (+). Finally, condition 10 is satisfied by satisfaction of rule (i) in I. This establishes the fact that I is an OWL direct interpretation.

Consider now any ontology O in {O₁,...,O_n}. To establish that I satisfies O, we need to establish that each axiom in the axiom closure of O is satisfied in I w.r.t. O. Note that, since O is normalized, it does not contain import statements, and thus the axiom closure of O is equal to O.

Consider any axiom d in O; d has one of the following forms (cf. the second column of Table Normalization of OWL 2 RL ontologies):

1. subproperty statement,
2. disjoint properties statement,
3. inverse property statement,
4. functional property statement,
5. symmetric property statement,
6. transitive property statement,
7. datatype definition,
8. has-key statement,
9. same-individual statement,
10. different-individuals statement, or
11. subclass statement SubClassOf(X Y).

Consider a subproperty statement SubObjectPropertyOf(p q) and a pair (k, l) in OP(<p>). Then, by construction of I, I_truth(I_frame(k)( I_C'(<p>), l ))) = t. But, by tr(d), it must be the case that also I_truth(I_frame(k)( I_C'(<q>), l ))) = t. But then, (k,l) must be in OP(<q>), by construction of I. This argument extends straightforwardly to subproperty statements with inverse or property-chain expressions. So, I satisfies d. Similar for statements of the forms 2--6.

Consider a datatype definition DatatypeDefinition( d e ), with d, e IRIs. This axiom is satisfied in I if DT(d) = DT(e). This definition is translated to the rules Forall ?x (?x[rdf:type -> e] :- ?x[rdf:type -> d]) Forall ?x (?x[rdf:type -> d] :- ?x[rdf:type -> e]) By satisfaction of these rules in I* and construction of I we have that I satisfies the datatype definition. This argument straightforwardly extends to more complex datatype definitions; recall that the only construct available in OWL 2 RL datatype definitions is intersection.

Consider a has-key axiom d. We have that every object in D*_ind, and thus also every object in IR is named. It is then straightforward to verify that if tr_O(d) is satisfied in I*, the condition in Section 2.3.5 of OWL2-Semantics is satisfied. Analogous for same-individual and different-individual axioms.

Consider the case that d is a subclass statement SubClassOf(X Y) and consider any k in C(X), where C is as in the Class Expressions Table in [OWL2-Semantics]. We show, by induction, that I* satisfies tr_O(X) when ?x is assigned to k.

If X is a classID, then satisfaction of tr(X) follows by an analogous argument as that for directives of form 1. Similar for value restrictions. If X is a some-value restriction of type Z on a property p, then there must be some object l such that (k,l) in OP(p) such that l is in C(Z).

By induction we have satisfaction of tr(Z) for some variable assignment. Then, by definition of I, we have I_truth(I_frame(k)( I_C'(<p>), l )) = t (true), thereby establishing satisfaction of tr_O(X) in I*. This extends straightforwardly to union, intersection, and one-of descriptions.

By satisfaction of tr_O(d), we have that tr_O(Y) is necessarily satisfied for ?x assigned to k. By an argument analogous to the argument above, we obtain that k is in C(Y).

This establishes satisfaction of d in I.

We obtain that every directive is satisfied in I. Therefore, O, and thus every ontology in C, is satisfied in I. We have established earlier that I* satisfies R' and not φ, so (I*, I) satisfies R' and not φ. We conclude that C does not entail φ.

(<=) Assume C does not RIF-OWL Direct-entail φ. This means there is a common-RIF-OWL Direct-interpretation (Î, I) that is a RIF-OWL Direct-model of C, but I is not a model of φ. To show that R* does not entail φ, we show that I is a model of R*.

R' is satisfied in I by assumption. Satisfaction of tr_O(O_i) can be shown analogously to establishment of satisfaction in I of O_i in the (=>) direction. We now establish satisfaction of the rules in R^OWL-Direct(V,R).

(i) follows immediately from the fact that C(owl:Nothing)={}. (ii) follows from conditions 2, 9, and 15 on OWL Direct interpretations. (iii) follows from conditions 3 and 9. (iv) follows from conditions 5, 6 and 9. (v) follows from conditions 5 and 9. (vi) follows from conditions 6 and 15. (vii) follows from conditions 8 and 9. (viii) and (ix) follow from condition 7. (x) follows from conditions 4 and 15.

This establishes satisfaction of R^OWL-Direct(V,R), and thus R*, in I. Therefore, R* does not entail φ.

  ☐

Entailment Theorem

Theorem Given a datatype map D conforming with T, a RIF-OWL DL-combination C=<R,{O₁,...,O_n}>, where {O₁,...,O_n} is an imports-closed set of OWL 2 RL ontologies with Vocabulary V, RIF-OWL Direct-entails a DL-condition formula φ with respect to D iff tr(merge({R, R^OWL-Direct(V), tr_O(tr_N(O₁)), ..., tr_O(tr_N(O_n))})) entails tr(φ).

Proof.

By the RIF-BLD DL-document formula Lemma,

tr(merge({R, R^OWL-Direct(V,R), tr_O(tr_N(O₁)), ..., tr_O(tr_N(O_n))})) entails tr(φ) iff merge({R, R^OWL-Direct(V,R), tr_O(tr_N(O₁)), ..., tr_O(tr_N(O_n))}) dl-entails φ.

Observe that the mapping tr() does not distinguish between frame formulas of the form a[rdf:type -> b] and membership formulas a#b. We may thus safely assume that R has no occurrences of the latter.

Then, by the Normalized Combination Embedding Lemma,

merge({R, R^OWL-DL(V), tr_O(tr_N(O₁)), ..., tr_O(tr_N(O_n))}) dl-entails φ iff <R,{tr_N(O₁),...,tr_N(O_n)}> RIF-OWL Direct-entails φ.

Finally, by the Normalization Lemma,

<R,{tr_N(O₁),...,tr_N(O_n)}> RIF-OWL Direct-entails φ iff C=<R,{O₁,...,O_n}> RIF-OWL Direct-entails φ.

This chain of equivalences establishes the theorem.   ☐

Satisfiability Theorem

Theorem Given a datatype map D conforming with T, a RIF-OWL Direct-combination <R,{O₁,...,O_n}>, where {O₁,...,O_n} is an imports-closed set of OWL 2 RL ontologies with Vocabulary V, is owl-dl-satisfiable with respect to D iff tr(merge({R, R^OWL-DL(V), tr_O(tr_N(O₁)), ..., tr_O(tr_N(O_n))}) does not entail rif:error.

Proof.

The theorem follows immediately from the previous theorem and the observation that a combination (respectively, document) is RIF-OWL Direct-satisfiable (respectively, has a model) if and only if it does not entail the condition formula "a"="b".   ☐