# SWC OWL Proofs

## Contents

## Embedding RDFS Entailment

**Theorem** A RIF-RDFS-satisfiable list-free RIF-RDF combination C=<*R*,{*S _{1}*,...,

*S*}> RIF-RDFS-entails a generalized RDF graph

_{n}*T*if and only if merge({

*R*,

*R*, tr

^{RDFS}_{R}(

*S*), ..., tr

_{1}_{R}(

*S*)}) entails tr

_{n}_{Q}(

*T*); C RIF-RDFS-entails a condition formula φ if and only if merge({

*R*,

*R*, tr

^{RDFS}_{R}(

*S*), ..., tr

_{1}_{R}(

*S*)}) entails φ.

_{n}Proof.In the proof we abbreviate merge({

R,R, tr^{RDFS}_{R}(S), ..., tr_{1}_{R}(S)}) with R'._{n}

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:Literalandrdfs:Resource, and show that I is an RDFS-interpretation and (**) in the (<=) direction we need to show thatis a model ofI'R.^{RDFS}

(*) In addition to the earlier assumptions about

, we assume that tr(I"s"^^rdf:XMLLiteral)[rdf:type -> rdfs:Literal]is not satisfied in, for any typed literal of the form (Is,rdf:XMLLiteral) inV._{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
kinD_{ind}such thatI_{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, andb∈D_{ind}such thatk≠I_{C}(rdf:type) orb≠I_{C}(rdfs:Resource), (a,b) ∈ IEXT(k) iffI_{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,...,_{1}S. It also does not affect satisfaction of the entailed graph or condition, since (by assumption) this does not contain a mention of_{n}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) inRfor every RDFS finite-axiomatic triple^{RDFS}t, the fact thatis a model ofIR, construction of I, and the extension of I in the proof of the RDF entailment embedding. Consider the RDFS semantic conditions:^{RDFS}

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 IP5 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 IC9 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

kinD_{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 valuekin LV. By definition, eitherkis in the value space of some considered datatype orI_{truth}(I_{frame}(k)(I_{C}(rdf:type),I_{C}(rdfs:Literal)))=t. In the latter case, clearlykis in ICEXT(I(rdfs:Literal)). In the former case,kis in the value space of some datatype with some labelD, and thusI_{truth}(I_{F}(I_{C}(pred:is))(Dk))=t. By the last rule inR, it must consequently be the case that^{RDFS}I_{truth}(I_{frame}(k)(I_{C}(rdf:type),I_{C}(rdfs:Literal)))=t, and thuskis 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

of the 2nd through the 12th rule in the definition ofIR.^{RDFS}This establishes the fact that I is an RDFS-interpretation.

(**) Consider

R. Satisfaction of^{RDFS}Rwas established in the proof in the previous section. Satisfaction of the facts corresponding to the RDFS axiomatic triples in^{RDF}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.I'

Satisfaction of the 1st through the 12th rule in

Rfollow 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^{RDFS}t, IL(t) is not in LV (by RDF semantic condition 3), ICEXT(rdfs:Literal)=LV, and the fact that theex:illxmlpredicate is only true for ill-typed XML literals. Finally, satisfaction of the last rule inRfollows from the fact that ICEXT(^{RDFS}rdfs:Literal)=LV, the definition of LV as a superset of the union of the value spaces of all datatypes, and the definition of thepred:ispredicates. This establishes the fact thatDis a model ofI'R. ☐^{RDFS}

**Theorem** A list-free RIF-RDF combination <*R*,{*S _{1}*,...,

*S*}> is RIF-RDFS-satisfiable if and only if merge({

_{n}*R*,

*R*, tr

^{RDFS}_{R}(

*S*), ..., tr

_{1}_{R}(

*S*)}) does not entail

_{n}`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-structurethat is a model of tr(R'), butÎ= <I,TV,DTS,DD_{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,DD_{ind},D_{func},I*_{C},I*_{C'},I_{V},I_{F},I*_{frame},I_{NF},I*_{sub},I*_{isa},I_{=},I_{external},I_{truth}>, withI*_{C'},I*_{frame},I*_{sub}, andI*_{isa}defined as follows: Lettbe an element insuch thatDI_{truth}(t)=tand letfinbe such thatDI_{truth}(f)=f.

- for every constant
c, withc'=tr'(c),I*_{C'}(c)=I_{C}(c');- for every constant
c'used as unary predicate symbol in tr(R) or tr(φ) such thatc'=tr'(c) for some constantc, and every objectkinD_{ind},I_{truth}(I_{F}(I_{C}(c'))(k))=tiffI*_{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 thatb'=tr'(b) for some constantb, and every pair (k, l) inD_{ind}×D_{ind},I_{truth}(I_{F}(I_{C}(b'))(k,l))=tiffI*_{frame}(k)((I_{C'}(b),l))=t,- if
I*_{frame}(k)((b,...,_{1}b))=_{n}tandI*_{frame}(k)((c,...,_{1}c))=_{m}tfor any two finite bags (b,...,_{1}b) and (_{n}c,...,_{1}c), then_{m}I*_{frame}(k)((b,...,_{1}b,_{n}c,...,_{1}c))=_{m}t;I*_{frame}(b)=ffor any other bag b;- for any two
k,l∈,DI*_{sub}(k,l)=tif for everyu∈,DI_{truth}(I_{F}(k)(u))=timpliesI_{truth}(I_{F}(l)(u))=t, otherwiseI*_{sub}(k,l)=f;- for any two
k,l∈,DI*_{isa}(k,l)=tifI_{truth}(I_{F}(k)(u))=t, otherwiseI*_{isa}(k,l)=f.

Observe that tr(R) and tr(φ) do not include frame formulas.

To show thatis a model ofÎ*Randis not a model of φ, we only need to show that (+) for any frame formulaI*a[b -> c]that is a DL-condition,is a model ofI*a[b -> c]iffis a model of tr(Ia[b -> c]). This argument straightforwardly extends to the case of frames with multiplebs and_{i}cs, since in RIF semantic structures the following condition is required to hold:_{i}TVal_{I}(a[b) =_{1}->c_{1}... b_{n}->c_{n}]tif and only ifTVal_{I}(a[b) = ... =_{1}->c_{1}]TVal_{I}(a[b) =_{n}->c_{n}]t[RIF-BLD]. The argument for formulasa # banda ## bis analogous.

Consider the caseb=rdf:type. Then,

is a model ofI*a[b -> c]iffI_{truth}(I*_{frame}((Ia))(I_{C'}(rdf:type),I_{C'}(c)))=t.

From the definition ofwe obtainI*

I_{truth}(I*_{frame}((Ia))(I_{C'}(rdf:type),I_{C'}(c)))=tiffI*_{frame}((Ia))(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 ofwe obtainI*

I*_{frame}((Ia))(I_{C'}(rdf:type),I_{C'}(c))=tiffI_{truth}(I_{F}(I_{C}(tr'(c)))((Ia)))=t.

Finally, since tr(a[b -> c])=tr'(c)(a), we obtain

I_{truth}(I_{F}(I_{C}(tr'(c)))((Ia)))=tiffis a model of tr(Ia[b -> c]).

From this chain of equivalences follows thatis a model ofI*a[b -> c]iffis a model of tr(Ia[b -> c]).

The argument for the caseb≠rdf:typeis analogous, thereby obtaining (+).

(<=) AssumeRdoes not dl-entail φ. This means there is some dl-semantic multi-structurethat is a model ofÎR, but= <I,TV,DTS,DD_{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 φ. Letbe the set of constant symbols occurring in the frame formulas of the formsBa[rdf:type -> b]anda[b -> c]inRor φ.

Consider the semantic multi-structure, which is obtained fromÎ*as follows:Î= <I*,TV,DTS,DD_{ind},D_{func},I*_{C},I_{V},I*_{F},I*_{frame},I_{NF},I_{sub},I_{isa},I_{=},I_{external},I_{truth}>. Lettandfinbe such thatDI_{truth}(t)=tandI_{truth}(f)=f. We defineI*_{C},I*_{frame}, andI*_{F}as follows:

I*_{C}(tr'(c))=I_{C'}(c) andI*_{C}(c)=I_{C}(c), for any constantcnot in the range of tr';I*_{frame}(b)=ffor any finite bag b of, andDI*_{F}is defined as follows:

- for every constant
c, given an objectkinD_{ind}, ifI_{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')=ffor any otherk'inD_{ind},- for every constant
c, given a pair (k, l) inD_{ind}×D_{ind}, ifI_{truth}(I_{frame}(k)((I_{C'}(c),l)))=t,I*_{F}(tr'(c))(k,l)=t;I*_{F}(tr'(c))(k',l')=ffor any other pair (k', l') inD_{ind}×D_{ind}, andI*_{F}(c)=I_{F}(c) for every other constantc.Observe that

Rand φ 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 _{1}*,...,

*O*}>, where

_{n}*O*,...,

_{1}*O*are simplified OWL 2 RL ontologies that do not import ontologies, C RIF-OWL Direct-entails φ iff C'=<

_{n}*R*,{tr

_{N}(

*O*),...,tr

_{1}_{N}(

*O*)}> RIF-OWL Direct-entails φ.

_{n}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Îis not a model of φ.I

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,...,_{1}O}, I satisfies tr_{n}_{N}(d), then I satisfiesO,..., and_{1}O, and thus (_{n}, I) satisfies C. SinceIis not a model of φ, C does not RIF-OWL Direct-entail φ.I

(<=) 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Î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 trI_{N}(O),..., and tr_{1}_{N}(O). So, (_{n}, 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 _{1}*,...,

*O*}>, where {

_{n}*O*,...,

_{1}*O*} is an imports-closed set of normalized OWL 2 RL ontologies with vocabulary

_{n}*V*, OWL Direct-entails a DL-condition φ with respect to D iff merge({

*R'*,

*R*(

^{OWL-Direct}*V*), tr

_{O}(

*O*), ..., tr

_{1}_{O}(

*O*)}) dl-entails φ, where

_{n}*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_{1}_{O}(O)} with R*._{n}

(=>) 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,DD_{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

Inamed for R*if for every objectk∈D_{ind}that is not in the value space of some datatype in,DTSk=I_{C}(c), wherecis either an IRI identifying an individual inVor a constant appearing as an individual inR. 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Î'is not a model of φ.I'

The set of unnamed individuals in

is the set of objectsIk∈D_{ind}that are not in the value space of some datatype in, and there is no IRIDTScidentifying an individual inVor constantcappearing as an individual inRsuch thatk=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,Îis not a model of φ: condition formulas do not contain negation, and so every condition formula that is satisfied byI'is also satisfied byI'.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. Since ψ does not contain negation, ψ is also satisfied byI'. 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 inIand construction ofI. Now, if there is a variableI'?xin the conclusion that does not appear in ψ,satisfies the conclusion for every assignment ofI?xto any element inD_{ind}. Since the individual domain ofis a strict subset ofI'D_{ind}, the conclusion is also satisfied in. Therefore,I'is a model of R*. In the remainder we assumeÎ'=Î.Î'

We define CExt(

c)={u|u∈D_{ind}andI_{truth}(I_{frame}(u)(rdf:type,I_{C}(c)))} as the class extension of the constantc. Furthermore, we defineD_{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}>, wheret,f∈such thatD*I_{truth}(t)=tandI*_{truth}(f)=f, and

D*_{ind}=D_{ind}union (union of the value spaces of all datatypes in D);=D*unionDD*_{ind};I*_{C}is likeI_{C}except that it maps all constants with symbol spaces in D\to the values in the in the corresponding datatypes, according to the respective lexical-to-value mappings;DTSI*_{frame}is defined as follows:

I*_{frame}(k)(I_{C'}(rdf:type),I_{C'}(rdfs:Literal))=tifk∈D_{D}, otherwiseI*_{frame}(k)(I_{C'}(rdf:type),I_{C'}(rdfs:Literal))=f,- otherwise
I*_{frame}is likeI_{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'), ifd'is a datatype identifier inVin the domain of D,- DT(
d') = set of all objectsksuch thatI_{truth}(I_{frame}(k)(I_{C'}(rdf:type),I_{C'}(<c>))) =t, for every datatype identifierd'inV, not in the domain of D,- C(
c) = set of all objectsksuch thatI_{truth}(I_{frame}(k)(I_{C'}(rdf:type),I_{C'}(<c>))) =t, for every class identifier inV,- OP(
p) = set of all pairs (k,l) such thatI_{truth}(I_{frame}(k)(I_{C'}(<p>),l))) =t(true), for every object property identifierpinVand not in {owl:topObjectProperty,owl:bottomObjectProperty};- OP(
owl:topObjectProperty) = IR × IR;- OP(
owl:bottomObjectProperty) = { };- DP(
p) = set of all pairs (k,l) such thatI_{truth}(I_{frame}(k)(I_{C'}(<p>),l))) =t(true), for every datatype property identifierpinVand 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) inV;- I(
i) =I_{C}(<i>) for every IRIiidentifying an individual inV;- 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

has a separation between the object and data domains: (+) each object is either in CExt(I*owl:Thing) or in CExt(rdfs:Literal) andD_{D}: each non-data value inD_{ind}is in CExt(owl:Thing) by rule (vii) and the fact thatis a named structure, and each data value is in CExt(I*rdfs:Literal) by construction of. The two sets are distinct by satisfaction of rule (ii) inI*.I

It is straightforward to see that

is a model of R* andÎ*is not a model of φ.I*

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:

- IR is a nonempty set,
- LV is a nonempty set disjoint with IR and including the value spaces of all datatypes in D,
- C :
V→ 2_{C}^{IR}- DT :
V→ 2_{D}^{LV}, where DT is the same as in D for each datatype d- OP :
V→ 2_{IP}^{IR×IR}- DP :
V→ 2_{DP}^{IR×LV}- LT : TL → LV, where TL is the set of typed literals in
Vand LT((s,d))=L2V(d)(s), for every typed literal (s,d) ∈_{L}V_{L}- I :
V→ IR_{I}- C(
owl:Thing) = IR- C(
owl:Nothing) = { }- OP(
owl:topObjectProperty) = IR × IR- DP(
owl:topDataProperty) = IR × LV- OP(
owl:bottomObjectProperty) = { }- DP(
owl:bottomDataProperty) = { }- DT(
rdfs:Literal) = LV

Condition 1 is met becauseis 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 ofD_{ind}and I, and the property (+). Finally, condition 10 is satisfied by satisfaction of rule (i) inI*. This establishes the fact that I is an OWL direct interpretation.I

Consider now any ontology

Oin {O,...,_{1}O}. To establish that I satisfies_{n}O, we need to establish that each axiom in the axiom closure ofOis satisfied in I w.r.t.O. Note that, sinceOis normalized, it does not contain import statements, and thus the axiom closure ofOis equal toO.

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):

- subproperty statement,
- disjoint properties statement,
- inverse property statement,
- functional property statement,
- symmetric property statement,
- transitive property statement,
- datatype definition,
- has-key statement,
- same-individual statement,
- different-individuals statement, or
- subclass statement
SubClassOf(.XY)

Consider a subproperty statementSubObjectPropertyOf(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 alsoI_{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 ), withd,eIRIs. This axiom is satisfied in I ifDT(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 inand 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.I*

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, the condition in Section 2.3.5 of OWL2-Semantics is satisfied. Analogous for same-individual and different-individual axioms.I*

Consider the case that d is a subclass statement

SubClassOf(and consider anyXY)kin C(), where C is as in the Class Expressions Table in [OWL2-Semantics]. We show, by induction, thatXsatisfies trI*_{O}() whenX?xis assigned tok.

If

is a classID, then satisfaction of tr(X) follows by an analogous argument as that for directives of form 1. Similar for value restrictions. IfXis a some-value restriction of typeXon a propertyZp, then there must be some objectlsuch that (k,l) in OP(p) such thatlis in C().ZBy induction we have satisfaction of tr(

) for some variable assignment. Then, by definition of I, we haveZI_{truth}(I_{frame}(k)(I_{C'}(<p>),l)) =t(true), thereby establishing satisfaction of tr_{O}() inX. This extends straightforwardly to union, intersection, and one-of descriptions.I*

By satisfaction of tr

_{O}(d), we have that tr_{O}() is necessarily satisfied forY?xassigned tok. By an argument analogous to the argument above, we obtain thatkis 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 thatsatisfiesI*R'and not φ, so (, I) satisfiesI*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Îis not a model of φ. To show that R* does not entail φ, we show thatIis a model of R*.I

R'is satisfied inby assumption. Satisfaction of trI_{O}(O) can be shown analogously to establishment of satisfaction in I of_{i}Oin the (=>) direction. We now establish satisfaction of the rules in_{i}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. Therefore, R* does not entail φ.I☐

## Entailment Theorem

**Theorem** Given a datatype map D conforming with T, a RIF-OWL DL-combination C=<*R*,{*O _{1}*,...,

*O*}>, where {

_{n}*O*,...,

_{1}*O*} is an imports-closed set of OWL 2 RL ontologies with Vocabulary

_{n}*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

_{1}_{O}(tr

_{N}(

*O*))})) entails tr(φ).

_{n}Proof.By the RIF-BLD DL-document formula Lemma,

tr(merge({

R,R(^{OWL-Direct}V,R), tr_{O}(tr_{N}(O)), ..., tr_{1}_{O}(tr_{N}(O))})) entails tr(φ) iff merge({_{n}R,R(^{OWL-Direct}V,R), tr_{O}(tr_{N}(O)), ..., tr_{1}_{O}(tr_{N}(O))}) dl-entails φ._{n}

Observe that the mapping tr() does not distinguish between frame formulas of the form

a[rdf:type -> b]and membership formulasa#b. We may thus safely assume thatRhas no occurrences of the latter.Then, by the Normalized Combination Embedding Lemma,

merge({

R,R(^{OWL-DL}V), tr_{O}(tr_{N}(O)), ..., tr_{1}_{O}(tr_{N}(O))}) dl-entails φ iff <_{n}R,{tr_{N}(O),...,tr_{1}_{N}(O)}> RIF-OWL Direct-entails φ._{n}

Finally, by the Normalization Lemma,

<

R,{tr_{N}(O),...,tr_{1}_{N}(O)}> RIF-OWL Direct-entails φ iff C=<_{n}R,{O,...,_{1}O}> RIF-OWL Direct-entails φ._{n}

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 _{1}*,...,

*O*}>, where {

_{n}*O*,...,

_{1}*O*} is an imports-closed set of OWL 2 RL ontologies with Vocabulary

_{n}*V*, is owl-dl-satisfiable with respect to D iff tr(merge({

*R*,

*R*(

^{OWL-DL}*V*), tr

_{O}(tr

_{N}(

*O*)), ..., tr

_{1}_{O}(tr

_{N}(

*O*))}) does not entail

_{n}`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". ☐