OWL Web Ontology Language
Semantics and Abstract Syntax
Appendix A. Proofs (Informative)

Editor:: Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies

Please refer to the errata for this document, which may include some normative corrections.

Appendix A. Proofs (Informative)

This appendix contains proofs of theorems contained in Section 5 of the document.

Nomenclature: Throughout this appendix D will be a datatype map (Section 3.1) containing datatypes for all the built-in OWL datatypes and rdf:XMLLiteral; T will be the mapping from abstract OWL ontologies to RDF graphs from Section 4.1; and VB will be the built-in OWL vocabulary. Also, the plain literals in a vocabulary will not be mentioned.

Note: Throughout this appendix all interpretations are with respect to the datatype map D. Thus all results are with respect to D. Some of the obvious details of the constructions are missing.

A.1 Correspondence between Abstract OWL and OWL DL

This section shows that the two semantics, the direct model theory for abstract OWL ontologies from Section 3, here called the direct model theory, and the OWL DL semantics from Section 5, here called the OWL DL model theory, correspond on certain OWL ontologies.

Definition: Given D as above, a separated OWL vocabulary (Section 4.2) is here further formalized into a set of URI references V', disjoint from the disallowed vocabulary (Section 4.2), with a disjoint partition of V', written as V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP, where the built-in OWL classes are in VC, the URI references all the datatype names of D and rdfs:Literal are in VD, the OWL built-in annotation properties are in VAP, and the OWL built-in ontology properties are in VXP.

Definition: The translation of a separated OWL vocabulary, V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP, written T(V'), consists of all the triples of the form
v rdf:type owl:Ontology . for v ∈ VO,
v rdf:type owl:Class . for v ∈ VC,
v rdf:type rdfs:Datatype . for v ∈ VD,
v rdf:type owl:Thing . for v ∈ VI,
v rdf:type owl:ObjectProperty . for v ∈ VOP,
v rdf:type owl:DatatypeProperty . for v ∈ VDP,
v rdf:type owl:AnnotationProperty . for v ∈ VAP, and
v rdf:type owl:OntologyProperty . for v ∈ VXP.

Definition: A collection of OWL DL ontologies and axioms and facts in abstract syntax form, O, (Section 2) with a separated vocabulary (Section 4) is here further formalized with the new notion of a separated vocabulary V = VO + VC + VD + VI + VOP + VDP + VAP + VXP, as follows:

All URI references used as ontology names are taken from VA, class IDs are taken from VC, datatype IDs are taken from VD, individual IDs are taken from VI, individual-valued property IDs are taken from VOP, data-valued property IDs are taken from VDP, annotation property IDs are taken from VAP, and ontology property IDs are taken from VXP.
All URI references used as individual IDs are given a type in some ontology in O.
The ontologies and axioms and facts in O only use the class-only vocabulary as class IDs; only use the datatype-only vocabulary as datatype IDs; only use the property-only vocabulary as datavaluedProperty IDs, individualvaluedProperty IDs, annotationProperty IDs, or ontologyProperty IDs; and do not mention any disallowed vocabulary.

The theorem to be proved is then: Let O and O' be collections of OWL DL ontologies and axioms and facts in abstract syntax form that are imports closed, such that their union has a separated vocabulary. Then O direct entails O' if and only if T(O) OWL DL entails T(O').

A.1.1 Correspondence for Descriptions

Lemma 1: Let V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP be a separated OWL vocabulary. Let V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Let I'= <R,EC,ER,L,S,LV> be a direct interpretation of V'. Let I = <R_I,P_I,EXT_I,S_I,L_I,LV_I> be a OWL DL interpretation of V that satisfies T(V'), with LV_I = LV. Let CEXT_I have its usual meaning, and, as usual, overload I to map any syntactic construct into its denotation. If

R = R_I
EC(v)=CEXT_I(S_I(v)), for v∈VC∪VD
ER(v)=EXT_I(S_I(v)), for v∈VOP∪VDP∪VAP∪VXP
< x, S(owl:DeprecatedClass) > ∈ ER(rdf:type) iff < x, S_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type)), for x ∈ R
< x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type) iff < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type)), for x ∈ R
L(d)=L_I(d), for d any typed data literal
S(v)=S_I(v) for v ∈ VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VO

then for d any abstract OWL description or data range over V',

I direct satisfies T(d), and
for any A mapping all the blank nodes of T(d) into R_I where I+A OWL DL satisfies T(d)
1. CEXT_I(I+A(M(T(d)))) = EC(d),
2. if d is a description then I+A(M(T(d)))∈CEXT_I(S_I(owl:Class)), and
3. if d is a data range then I+A(M(T(d)))∈CEXT_I(S_I(rdfs:Datatype)).

Proof:

The proof of the lemma is by a structural induction. Throughout the proof, let IOT = CEXT_I(I(owl:Thing)), IOC = CEXT_I(I(owl:Class)), IDC = CEXT_I(I(rdfs:Datatype)), IOOP = CEXT_I(I(owl:ObjectProperty)), IODP = CEXT_I(I(owl:DatatypeProperty)), and IL = CEXT_I(I(rdf:List)).

To make the induction work, it is necessary to show that for any d a description or data range with sub-constructs T(d) contains triples for each of the sub-constructs that do not share any blank nodes with triples from the other sub-constructs. This can easily be verified from the rules for T.

If p∈VOP then I satisfies p∈IOOP. Then, as I is an OWL DL interpretation, I satisfies <p,I(owl:Thing)>∈EXT_I(I(rdfs:domain)) and <p,I(owl:Thing)>∈EXT_I(I(rdfs:range)). Thus I satisfies T(p). Similarly for p∈VDP.

Base Case: v ∈ VC, including owl:Thing and owl:Nothing: As v∈VC and I satisfies T(V), thus I(v)∈CEXT_I(I(owl:Class)). Because I is an OWL DL interpretation CEXT_I(I(v))⊆IOT, so <I(v),I(owl:Thing)>∈EXT_I(I(rdfs:subClassOf)). Thus I OWL DL satisfies T(v). As M(T(v)) is v, thus CEXT_I(I(M(T(v))))=EC(v). Finally, from above, I(v)∈IOC.
Base Case: v ∈ VD, including rdfs:Literal: As v∈VD and I satisfies T(V), thus I(v)∈CEXT_I(I(rdfs:Datatype)). Because I is an OWL DL interpretation CEXT_I(I(v))⊆LV_I, so <I(v),I(rdfs:Literal)>∈EXT_I(I(rdfs:subClassOf)). Thus I RDF-compatibile satisfies T(v). As M(T(v)) is v, thus CEXT_I(I(M(T(v))))=EC(v). Finally, from above I(v)∈IDC.
Base Case: d=oneOf(i₁…i_n), where the i_j are individual IDs: As i_j∈VI for 1≤j≤n and I satisfies T(V), thus I(i_j)∈IOT. The second comprehension principle for sequences then requires that there is some l∈IL that is a sequence of I(i₁),…,I(i_n) over IOT. For any l that is a sequence of I(i₁),…,I(i_n) over IOT the comprehension principle for oneOf requires that there is some y∈CEXT_I(I(rdfs:Class)) such that <y,l> ∈ EXT_I(IS(owl:oneOf)). From the third characterization of oneOf, y∈IOC. Therefore I satisfies T(d). For any I+A that satisfies T(d), CEXT_I(I+A(M(T(d)))) = {I(i₁),…,I(i_n)} = EC(d). Finally, I+A(M(T(d)))∈IOC.
Base Case: d=oneOf(v₁…v_n), where the v_i are data literals: Because I(v_j)∈LV_I, the second comprehension principle for sequences then requires that there is some l∈IL that is a sequence of I(v₁),…,I(v_n) over LV_I. For any l that is a sequence of I(v₁),…,I(v_n) over LV_I the comprehension principle for oneOf requires that there is some y∈CEXT_I(I(rdfs:Class)) such that <y,l> ∈ EXT_I(IS(owl:oneOf)). From the second characterization of oneOf, y∈IOC. Therefore I satisfies T(d). For any I+A that satisfies T(d), CEXT_I(I+A(M(T(d)))) = {I(i₁),…,I(i_n)} = EC(d). Finally, I+A(M(T(d)))∈IDC.
Base Case: d=restriction(p value(i)), with p∈VOP∪VDP and i an individualID: As p∈VOP∪VDP, from above I satisfies T(p). As I satisfies T(V'), I(p)∈IOOP∪IODP. As i∈VI and I satisfies T(V'), I(i)∈IOT. From a comprehension principle for restriction, I satisfies T(d). For any A such that I+A satisfies T(d), CEXT_I(I+A(M(T(d)))) = { x∈IOT | <x,I(i)> ∈ EXT_I(p) } = { x∈R | <x,S(i)> ∈ ER(p) } = EC(d). Finally, I+A(M(T(d)))∈IOC.
Base Case: d=restriction(p value(i)), with p∈VOP∪VDP and i a typed data value.: Similar.
Base Case: d=restriction(p minCardinality(n)), with p∈VOP∪VDP and n a non-negative integer: Similar.
Base Case: d=restriction(p maxCardinality(n)), with p∈VOP∪VDP and n a non-negative integer: Similar.
Base Case: d=restriction(p Cardinality(n)), with p∈VOP∪VDP and n a non-negative integer: Similar.
Inductive Case: d=complementOf(d'): From the induction hypothesis, I satisfies T(d'). As d' is a description, from the induction hypothesis there is a mapping, A, that maps all the blank nodes in T(d') into domain elements such that I+A satisfies T(d') and I+A(M(T(d'))) = EC(d') and I+A(M(T(d')))∈IOC. The comprehension principle for complementOf then requires that there is a y∈IOC such that I+A satisfies <y,e>∈EXT_I(I(owl:complementOf)) so I satisfies T(d). For any I+A that satisfies T(d), CEXT_I(I+A(M(T(d)))) = IOT-CEXT_I(I+A(M(T(d)))) = R-EC(d') = EC(d). Finally, I+A(M(T(d)))∈IOC.
Inductive Case: d = unionOf(d₁ … d_n): From the induction hypothesis, I satisfies d_i for 1≤i≤n so there is a mapping, A_i, that maps all the blank nodes in T(d_i) into domain elements such that I+A_i satisfies T(d_i). As the blank nodes in T(d_i) are disjoint from the blank nodes of T(d_j) for i≠j, I+A₁+…+A_n, and thus I, satisfies T(d_i)∪…∪T(d_n). Each d_i is a description, so from the induction hypothesis, I+A₁+…+A_n(M(T(d_i)))∈IOC. The first comprehension principle for sequences then requires that there is some l∈IL that is a sequence of I+A₁+…+A_n(M(T(d₁))),…, I+A₁+…+A_n(M(T(d_n))) over IOC. The comprehension principle for unionOf then requires that there is some y∈IOC such that <y,l>∈EXT_I(I(owl:unionOf)) so I satisfies T(d).
For any I+A that satisfies T(d), I+A satisfies T(d_i) so CEXT_I(I+A(d_i)) = EC(d_i)). Then CEXT_I(I+A(M(T(d)))) = CEXT_I(I+A(d₁))∪…∪CEXT_I(I+A(d_n)) = EC(d₁)∪…∪EC(d_n) = EC(d). Finally, I(M(T(d)))∈IOC.
Inductive Case: d = intersectionOf(d₁ … d_n): Similar.
Inductive Case: d = restriction(p x₁ x₂ … x_n): As p∈VOP∪VDP, from above I satisfies T(p). From the induction hypothesis, I satisfies restriction(p x_i) for 1≤i≤n so there is a mapping, A_i, that maps all the blank nodes in T(restriction(p x_i)) into domain elements such that I+A_i satisfies T(restriction(p x_i)). As the blank nodes in T(restriction(p x_i)) are disjoint from the blank nodes of T(restriction(p x_j)) for i≠j, I+A₁+…+A_n, and thus I, satisfies T(restriction(p x₁ … x_n)). Each restriction(p x_i) is a description, so from the induction hypothesis, M(T(restriction(p x_i)))∈IOC. The first comprehension principle for sequences then requires that there is some l∈IL that is a sequence of I+A₁+…+A_n(M(T(restriction(p x_i)))),…, I+A₁+…+A_n(M(T(restriction(p x_i)))) over IOC. The comprehension principle for intersectionOf then requires that there is some y∈IOC such that <y,l>∈EXT_I(I(owl:intersectionOf)) so I satisfies T(d).
For any I+A that satisfies T(d) I+A satisfies T(d_i) so CEXT_I(I+A(d_i)) = EC(d_i)). Then CEXT_I(I+A(M(T(d)))) = CEXT_I(I+A(restriction(p x_i)))∩…∩ CEXT_I(I+A(restriction(p x_n))) = EC(restriction(p x_i))cap;…∩EC(restriction(p x_i)) = EC(d). Finally, I(M(T(d)))∈IOC.
Inductive Case: d = restriction(p allValuesFrom(d')), with p∈VOP∪VDP and d' a description: As p∈VOP∪VDP, from above I satisfies T(p). From the induction hypothesis, I satisfies T(d'). As d' is a description, from the induction hypothesis, any mapping, A, that maps all the blank nodes in T(d') into domain elements such that I+A satisfies T(d') has I+A(M(T(d'))) = EC(d') and I+A(M(T(d')))∈IOC. As p∈VOP∪VDP and I satisfies T(V'), I(p)∈IOOP∪IODP. The comprehension principle for allValuesFrom restrictions then requires that I satisfies the triples in T(d) that are not in T(d') or T(p) in a way that shows that I satisfies T(d).
For any I+A that satisfies T(d), CEXT_I(I+A(M(T(d)))) = {x∈IOT | ∀ y∈IOT : <x,y>∈EXT_I(p) implies y∈CEXT_I(M(T(d')))} = {x∈R | ∀ y∈R : <x,y>∈ER(p) implies y∈EC(d')} = EC(d). Finally, I+A(M(T(d)))∈IOC.
Inductive Case: d = restriction(p someValuesFrom(d)) with p∈VOP∪VDP and d' a description: Similar.
Inductive Case: d = restriction(p allValuesFrom(d)) with p∈VOP∪VDP and d' a data range: Similar.
Inductive Case: d = restriction(p someValuesFrom(d)) with p∈VOP∪VDP and d' a data range: Similar.

Lemma 1.1: Let V', V, I', and I be as in Lemma 1. Let d be an abstract OWL individual construct over V', (of the form Individual(…)). Then for any A mapping all the blank nodes of T(d) into R_I where I+A OWL DL satisfies T(d), I+A(M(T(d))) ∈ EC(d). Also, for any r ∈ EC(d) there is some A mapping all the blank nodes of T(d) into R_I such that I+A(M(T(d))) = r.

Proof:

A simple inductive argument shows that I+A(M(T(d))) must satisfy all the requirements of EC(d). Another inductive argument, depending on the non-sharing of blank nodes in sub-constructs, shows that for each r ∈ EC(d) there is some A such that I+A(M(T(d))) = r.

A.1.2 Correspondence for Directives

Lemma 1.9: Let V', V, I', and I be as in Lemma 1. Let F be an OWL directive over V' with an annotation of the form annotation(p x). If F is a class or property axiom, let n be the name of the class or property. If F is an individual axiom, let n be the main node of T(F). Then for any A mapping all the blank nodes of T(F) into R_I, I+A OWL DL satisfies the triples resulting from the annotation iff I' direct satisfies the conditions resulting from the annotation.

Proof:

For annotations to URI references, the lemma can be easily established by an inspection of the semantic condition and the translation triples. For annotations to Individual(…), the use of Lemma 1.1 is also needed.

Lemma 2: Let V', V, I', and I be as in Lemma 1. Let F be an OWL directive over V'. Then I satisfies T(F) iff I' satisfies F.

Proof:

The main part of the proof is a structural induction over directives. Annotations occur in many directives and work exactly the same so they just require a use of Lemma 1.9. The rest of the proof will thus ignore annotations. Deprecations can be handled in a similar fashion and will also be ignored in the rest of the proof.

Case: F = Class(foo complete d₁ … d_n).

Let d=intersectionOf(d₁ … d_n). As d is a description over V', thus I satisfies T(d) and for any A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_I(I+A(M(T(d)))) = EC(d). Thus for any sub-description of d, d', CEXT_I(I+A(M(T(d')))) = EC(d'), and I+A(M(T(d')))∈IOC. Thus for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_I(I+A(M(T(d)))) = EC(d) and I+A(M(T(d)))∈IOC; and for each d' a sub-description of d, CEXT_I(I+A(M(T(d')))) = EC(d'), and I+A(M(T(d')))∈IOC.

If I' satisfies F then EC(foo) = EC(d). From above, there is some A such that CEXT_I(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(I(foo)) and I+A(M(T(d)))∈IOC. Because I satisfies T(V), I(foo)∈IOC, thus <I(foo),I+A(M(T(d)))> ∈ EXT_I(I(owl:equivalentClass)). Further, because of the semantic conditions on I(owl:intersectionOf), <I(foo),I+A(M(T(SEQ d₁ … d_n)))> ∈ EXT_I(I(owl:intersectionOf)).

If d is of the form intersectionOf(d₁) then CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) and I+A(M(T(d₁)))∈IOC. So, from the semantic conditions on I(owl:equivalentClass), <I(foo),I+A(M(T(d₁)))> ∈ EXT_I(I(owl:equivalentClass)). If d₁ is of the form complementOf(d'₁) then IOT - CEXT_I(I+A(M(T(d'₁)))) = CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) and I+A(M(T(d'₁)))∈IOC. So, from the semantic conditions on I(owl:complementOf), <I(foo),I+A(M(T(d'₁)))> ∈ EXT_I(I(owl:complementOf)). If d₁ is of the form unionOf(d₁₁ … d_1m) then CEXT_I(I+A(M(T(d₁₁)))) ∪ … ∪ CEXT_I(I+A(M(T(d_1m)))) = CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) and I+A(M(T(d_1j)))∈IOC, for 1≤ j ≤ m. So, from the semantic conditions on I(owl:unionOf), <I(foo),I+A(M(T(SEQ d₁₁ … d_1m)))> ∈ EXT_I(I(owl:unionOf)).

Therefore I satisfies T(F), for each potential T(F).

If I satisfies T(F) then I satisfies T(intersectionOf(d₁ … d_n)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXT_I(I(owl:equivalentClass)). Thus EC(d) = CEXT_I(I+A(M(T(d)))) = CEXT_I(I(foo)) = EC(foo). Therefore I' satisfies F.

Case: F = Class(foo partial d₁ … d_n)

Let d=intersectionOf(d₁ … d_n). As d is a description over V', thus I satisfies T(d) and for any A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_I(I+A(M(T(d)))) = EC(d). Thus CEXT_I(I+A(M(T(d_i)))) = EC(d_i), for 1 ≤ i ≤ n. Thus for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), CEXT_I(I+A(M(T(d_i)))) = EC(d_i), and I+A(M(T(d_i))∈IOC, for 1 ≤ i ≤ n.

If I' satisfies F then EC(foo) ⊆ EC(d_i), for 1 ≤ i ≤ n. From above, there is some A such that CEXT_I(I+A(M(T(d_i)))) = EC(d_i) ⊇ EC(foo) = CEXT_I(I(foo)) and I+A(M(T(d_i))∈IOC. Because I satisfies T(V), I(foo)∈IOC, thus <I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf)), for 1 ≤ i ≤ n. Therefore I satisfies T(F).

If I satisfies T(F) then I satisfies T(d_i), for 1 ≤ i ≤ n. Thus there is some A as above such that <I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf)), for 1 ≤ i ≤ n. Thus EC(d) = CEXT_I(I+A(M(T(d_i)))) ⊇ CEXT_I(I(foo)) = EC(foo), for 1 ≤ i ≤ n. Therefore I' satisfies F.

Case: F = EnumeratedClass(foo i₁ … i_n)

Let d=oneOf(i₁ … i_n). As d is a description over V' so I satisfies T(d) and for some A mapping the blank nodes of T(d) such that I+A satisfies T(d), EC(d) = CEXT_I(I+A(M(T(d)))) = {S_I(M(T(i₁)), … S_I(M(T(i_n))} Also, S_I(M(T(i_j)) ∈ IOT, for 1 ≤ j ≤ n.

If I' satisfies F then EC(foo) = EC(d). From above, there is some A such that CEXT_I(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(I(foo)) and I+A(M(T(d))∈IOC. Let e be I+A(M(T(SEQ i₁ … i_n))). Then, from the semantic conditions on I(owl:oneOf), <I(foo),e> ∈ EXT_I(I(owl:oneOf)). Therefore I satisfies T(F).

If I satisfies T(F) then I satisfies T(SEQ i₁ … i_n). Thus there is some A as above such that <I(foo),I+A(M(T(SEQ i₁ … i_n)))> ∈ EXT_I(I(owl:oneOf)). Thus {S_I(M(T(i₁)), …, S_I(M(T(i_n))} = CEXT_I(I(foo)) = EC(foo). Therefore I' satisfies F.

Case: F = Datatype(foo)

The only thing that needs to be shown here is the typing for foo, which is similar to that for classes.

Case: F= DisjointClasses(d₁ … d_n)

As d_i is a description over V' therefore I satisfies T(d_i) and for any A mapping the blank nodes of T(d_i) such that I+A satisfies T(d_i), CEXT_I(I+A(M(T(d_i)))) = EC(d_i).

If I satisfies T(F) then for 1≤i≤n there is some A_i such that I satisfies <I+A_i(M(T(d_i))),I+A_j(M(T(d_j)))> ∈ EXT_I(I(owl:disjointWith)) for each 1≤i<j≤n. Thus EC(d_i)∩EC(d_j) = {}, for i≠j. Therefore I' satisfies F.

If I' satisfies F then EC(d_i)∩EC(d_j) = {} for i≠j. For any A_i and A_j as above <I+A_i+A_j(M(T(d_i))),I+A_i+A_j(M(T(d_j)))> ∈ EXT_I(I(owl:disjointWith)), for i≠j. As at least one A_i exists for each i, and the blank nodes of the T(d_j) are all disjoint, I+A₁+…+A_n satisfies T(DisjointClasses(d₁ … d_n)). Therefore I satisfies T(F).

Case: F = EquivalentClasses(d₁ … d_n)

Similar.

Case: F = SubClassOf(d₁ d2)

Somewhat similar.

Case: F = ObjectProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_k) [inverse(i)] [Symmetric] [Functional] [InverseFunctional] [OneToOne] [Transitive])

As d_i for 1≤i≤m is a description over V' therefore I satisfies T(d_i) and for any A mapping the blank nodes of T(d_i) such that I+A satisfies T(d_i), CEXT_I(I+A(M(T(d_i)))) = EC(d_i). Similarly for r_i for 1≤i≤k.

If I' satisfies F, then, as p∈VOP, I satisfies I(p)∈IOOP. Then, as I is an OWL DL interpretation, I satisfies <I(p),I(owl:Thing)>∈EXT_I(I(rdfs:domain)) and <I(p),I(owl:Thing)>∈EXT_I(I(rdfs:range)). Also, ER(p)⊆ER(s_i) for 1≤i≤n, so EXT_I(I(p))=ER(p) ⊆ ER(s_i)=EXT_I(I(s_i)) and I satisfies <I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf)). Next, ER(p)⊆EC(d_i)×R for 1≤i≤m, so <z,w>∈ER(p) implies z∈EC(d_i) and for any A such that I+A satisfies T(d_i), <z,w>∈EXT_I(p) implies z∈CEXT_I(I+A(M(T(d_i)))) and thus <I(p),I+A(M(T(d_i)))>∈EXT_I(I(rdfs:domain)). Similarly for r_i for 1≤i≤k.

If I' satisfies F and inverse(i) is in F, then ER(p) and ER(i) are converses. Thus <u,v>∈ER(p) iff <v,u>∈ER(i) so <u,v>∈EXT_I(p) iff <v,u>∈EXT_I(i) and I satisfies <I(p),I(i)>∈EXT_I(I(owl:inverseOf)). If I' satisfies F and Symmetric is in F, then ER(p) is symmetric. Thus if <x,y>∈ ER(p) then <y,x>∈ER(p) so if <x,y> ∈ EXT_I(p) then <y, x>∈EXT_I(p). and thus I satisfies p∈CEXT_I(I(owl:Symmetric)). Similarly for Functional, InverseFunctional, and Transitive. Thus if I' satisfies F then I satisfies T(F).

If I satisfies T(F) then, for 1≤i≤n, <I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf)) so ER(p)=EXT_I(I(p)) ⊆ EXT_I(I(s_i))=ER(s_i). Also, for 1≤i≤m, for some A such that I+A satisfies T(d_i), <I(p),I+A(M(T(d_i)))>∈EXT_I(I(rdfs:domain)) so <z,w>∈EXT_I(p) implies z∈CEXT_I(I+A(M(T(d_i)))). Thus <z,w>∈ER(p) implies z∈EC(d_i) and ER(p)⊆EC(d_i)×R. Similarly for r_i for 1≤i≤k.

If I satisfies T(F) and inverse(i) is in F, then I satisfies <I(p),I(i)>∈EXT_I(I(owl:inverseOf)). Thus <u,v>∈EXT_I(p) iff <v,u>∈EXT_I(i) so <u,v>∈ER(p) iff <v,u>∈ER(i) and ER(p) and ER(i) are converses. If I satisfies F and Symmetric is in F, then I satisfies p∈CEXT_I(I(owl:Symmetric)) so if <x,y> ∈ EXT_I(p) then <y, x>∈EXT_I(p). Thus if <x,y>∈ ER(p) then <y,x>∈ER(p) and ER(p) is symmetric. Similarly for Functional, InverseFunctional, and Transitive. Thus if I satisfies T(F) then I' satisfies F.

Case: F = DatatypeProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_l) [Functional])

Similar, but simpler.

Case: F = AnnotationProperty(p domain(d₁) … domain(d_m))

Similar, but even simpler.

Case: F = OntologyProperty(p domain(d₁) … domain(d_m))

Similar, but even simpler.

Case: F = EquivalentProperties(p₁ … p_n), for p_i∈VOP

As p_i∈VOP and I satisfies T(V'), I(p_i)∈IOOP. If I satisfies T(F) then <I(p_i),I(p_j)> ∈ EXT_I(I(owl:equivalentProperty)), for each 1≤i<j≤n. Therefore EXT_I(p_i) = EXT_I(p_j), for each 1≤i<j≤n; ER(p_i) = ER(p_j), for each 1≤i<j≤n; and I' satisfies F.

If I' satisfies F then ER(p_i) = ER(p_j), for each 1≤i<j≤n. Therefore EXT_I(p_i) = EXT_I(p_j), for each 1≤i<j≤n. From the OWL DL definition of owl:equivalentProperty, <I(p_i),I(p_j)> ∈ EXT_I(I(owl:equivalentProperty)), for each 1≤i<j≤n. Thus I satisfies T(F).

Case: F = SubPropertyOf(p₁ p₂)

Somewhat similar, but simpler.

Case: F = SameIndividual(i₁ … i_n)

Similar to SamePropertyAs.

Case: F = DifferentIndividuals(i₁ … i_n)

Similar to SamePropertyAs.

Case: F = Individual([i] type(t₁) … type(t_n) value(p₁ v₁) … value(p_n v_n))

If I satisfies T(F) then there is some A that maps each blank node in T(F) such that I+A satisfies T(F). A simple examination of T(F) shows that the mappings of A plus the mappings for the individual IDs in F, which are all in IOT, show that I' satisfies F.

If I' satisfies F then for each Individual construct in F there must be some element of R that makes the type relationships and relationships true in F. The triples in T(F) then fall into three categories. 1/ Type relationships to owl:Thing, which are true in I because the elements above belong to R. 2/ Type relationships to OWL descriptions, which are true in I because they are true in I', from Lemma 1. 3/ OWL property relationships, which are true in I' because they are true in I. Thus I satisfies T(F).

A.1.3 From RDF Semantics to Direct Semantics

Lemma 3: Let V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP be a separated OWL vocabulary. Let V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Then for every OWL DL interpretation I = <R_I,P_I,EXT_I,S_I,L_I,LV_I> of V that satisfies T(V') there is an direct interpretation I' of V' such that for any collection of OWL abstract ontologies and axioms and facts O with vocabulary V' such that O is imports closed, I' direct satisfies O iff I OWL DL satisfies T(O).

Proof:

Let CEXT_I be defined as usual from I. The required direct interpretation will be I' = < R_I, EC, ER, L, S, LV_I > where

EC(v) = CEXT_I(S_I(v)), for v∈VC∪VD
ER(v) = EXT_I(S_I(v)), for v∈VOP∪VDP∪VAP∪VXP
< x, S(owl:DeprecatedClass) > ∈ ER(rdf:type) iff < x, S_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type)), for x ∈ R
< x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type) iff < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type)), for x ∈ R
L(d) = L_I(d), for d a typed literal
S(v) = S_I(v), for n∈VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VO

V', V, I', and I meet the requirements of Lemma 2, so for any directive D over V' I satisfies T(D) iff I' satisfies D.

Because O is imports closed, O includes all the ontologies that would be imported in T(O) so the importing part of imports directives will be handled the same. Satisfying an abstract ontology is just satisfying its directives and satisfying the translation of an abstract ontology is just satisfying all the triples so I OWL DL satisfies T(K) iff I' direct satisfies K.

A.1.4 From Direct Semantics to RDF Semantics

Lemma 4: Let V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP be a separated OWL vocabulary. Let V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VB. Then for every direct interpretation I' = < U, EC, ER, L, S, LV > of V' there is an OWL DL interpretation I of V that satisfies T(V') such that for any collection of OWL abstract ontologies and axioms and facts O with vocabulary V' such that O is imports closed, I' direct satisfies O iff I OWL DL satisfies T(O).

Proof:

Construct I = < R_I, P_I, EXT_I, S_I, L, LV_I > as follows:

Let IOC be all the OWL descriptions over V', plus the class-only vocabulary.
Let IDC be all the OWL data ranges over V'.
Let IOP = VOP ∪ VDP ∪ VAP ∪ VXP, plus the property-only vocabulary.
Let IX = VO.
Let IL be rdf:nil plus finite sequences over U, over IOC, and over LV.
Let IAD be rdf:nil plus the finite sequences over U.
Let IV be the disallowed vocabulary minus rdf:nil.
Let R_I be the disjoint union of U, IOC, IDC, IOP, IX, IL, IAD, and IV.
Let P_I be IOP ∪ IV
Let LV_I = LV.
Let S_I(n) = S(n) for n∈VI.
Let S_I(n) = n for n∈V-VI.
For c∈IOC, CEXT_I(c)=EC(c), if defined, otherwise {}.
For d∈IDC, CEXT_I(d)=EC(d).
For x∈U∪IL∪IAD∪IOP∪IX, CEXT_I(x)={}.
CEXT_I(S_I(rdf:type)) = {}
CEXT_I(S_I(rdf:Property)) = P_I
CEXT_I(S_I(rdf:List)) = IL
CEXT_I(S_I(rdf:XMLLiteral)) is the RDF XML literal values
CEXT_I(S_I(rdf:first))= CEXT_I(S_I(rdf:rest)) = CEXT_I(S_I(rdfs:domain)) = CEXT_I(S_I(rdfs:range)) = {}
CEXT_I(S_I(rdfs:Resource)) = R_I
CEXT_I(S_I(rdfs:Literal)) = LV_I
CEXT_I(S_I(rdfs:Datatype)) = D
CEXT_I(S_I(rdfs:Class)) = IOC ∪ IV
CEXT_I(S_I(rdfs:subClassOf)) = CEXT_I(S_I(rdfs:subPropertyOf)) = CEXT_I(S_I(rdfs:member)) = {}
CEXT_I(S_I(rdfs:Container)) = CEXT_I(S_I(rdf:Seq)) ∪ CEXT_I(S_I(rdf:Bag)) ∪ CEXT_I(S_I(rdf:Alt))
CEXT_I(S_I(rdfs:ContainerMembershipProperty)) is the RDF container membership properties
For r∈IOP, EXT_I(r)=ER(r), if defined, otherwise {}.
EXT_I(S_I(rdf:type)) is determined by CEXT_I.
EXT_I(S_I(rdf:Property)) = EXT_I(S_I(rdf:List)) = EXT_I(S_I(rdf:XMLLiteral)) = {}
<x,y> ∈ EXT_I(rdf:first) iff x∈IL and y is its first element
<x,y> ∈ EXT_I(rdf:rest) iff x∈IL and y is its tail
EXT_I(S_I(rdfs:domain)) = { <x,y> : x∈IOP y∈IOC ∧ ∀ w, <w,z> ∈ EXT_I(x) implies w ∈ CEXT_I(y) }
EXT_I(S_I(rdfs:range)) = { <x,y> : x∈OP y∈IOC ∧ ∀ z, <w,z> ∈ EXT_I(x) implies z ∈ CEXT_I(y) }
EXT_I(S_I(rdfs:Resource)) = EXT_I(S_I(rdfs:Literal)) = EXT_I(S_I(rdfs:Datatype)) = EXT_I(S_I(rdfs:Class)) = {}
EXT_I(S_I(rdfs:subClassOf)) = { <x,y> : x,y∈IOC ∧ CEXT_I(x) ⊆ CEXT_I(y) }
EXT_I(S_I(rdfs:subPropertyOf)) = { <x,y> : x,y∈OP ∧ EXT_I(x) ⊆ EXT_I(y) }
EXT_I(S_I(rdfs:member)) is the union of the extensions of the container membership properties
EXT_I(S_I(rdfs:Container)) = EXT_I(S_I(rdfs:ContainerMembershipProperty)) = {}
The extensions of owl:allValuesFrom, owl:cardinality, owl:hasValue, owl:maxCardinality, owl:minCardinality, owl:onProperty, and owl:someValuesFrom are as necessary to link the elements of IOC and IDC up with their parts. Their class extensions are all empty.
The extensions of owl:complementOf, owl:intersectionOf, owl:oneOf, and owl:unionOf are as necessary to make their semantic conditions work out correctly. Their class extensions are all empty. This can easily be done here because modifying these extensions does not induce any loops in the process.
CEXT_I(S_I(owl:AnnotationProperty)) = VAP
CEXT_I(S_I(owl:OntologyProperty)) = VXP
CEXT_I(S_I(owl:Class)) = IOC
CEXT_I(S_I(owl:DatatypeProperty)) = VDP
CEXT_I(S_I(owl:FunctionalProperty)) is those elements of VOP∪VDP whose extension is partial functional
CEXT_I(S_I(owl:InverseFunctionalProperty)) is those elements of VOP whose extension is inverse partial functional
CEXT_I(S_I(owl:ObjectProperty)) = VOP
CEXT_I(S_I(owl:Ontology)) = VO
CEXT_I(S_I(owl:Restriction)) is those elements of IOC that are OWL restrictions
CEXT_I(S_I(owl:SymmetricProperty)) is those elements of VOP whose extension is symmetric
CEXT_I(S_I(owl:TransitiveProperty)) is those elements of VOP whose extension is transitive
EXT_I(S_I(owl:AnnotationProperty)) = EXT_I(S_I(owl:OntologyProperty)) = EXT_I(S_I(owl:Class)) = EXT_I(S_I(owl:DatatypeProperty)) = EXT_I(S_I(owl:FunctionalProperty)) = EXT_I(S_I(owl:InverseFunctionalProperty)) = EXT_I(S_I(owl:ObjectProperty)) = EXT_I(S_I(owl:Ontology)) = EXT_I(S_I(owl:Restriction)) = EXT_I(S_I(owl:SymmetricProperty)) = EXT_I(S_I(owl:TransitiveProperty)) = {}
CEXT_I(S_I(owl:AllDifferent)) consists of those elements of IAD that have an owl:distinctMembers property
EXT_I(S_I(owl:differentFrom)) is the inequality relation on U
EXT_I(S_I(owl:disjointWith)) relates members of IOC that have the disjoint class extensions
EXT_I(S_I(owl:distinctMembers)) relates elements of IAD to their copy in IL, but only for sequences of distinct individuals
EXT_I(S_I(owl:equivalentClass)) relates members of IOC that have the same class extension
EXT_I(S_I(owl:equivalentProperty)) relates members of IOP∪IDP that have the same extension
EXT_I(S_I(owl:inverseOf)) relates members of IOP whose extensions are inverses of each other
EXT_I(S_I(owl:sameAs)) is the equality relation on U
EXT_I(S_I(owl:AllDifferent)) = CEXT_I(S_I(owl:differentFrom)) = CEXT_I(S_I(owl:disjointWith)) = CEXT_I(S_I(owl:distinctMembers)) = CEXT_I(S_I(owl:equivalentClass)) = CEXT_I(S_I(owl:equivalentProperty)) = CEXT_I(S_I(owl:inverseOf)) = CEXT_I(S_I(owl:sameAs)) = {}
CEXT_I(S_I(owl:DeprecatedClass)) = { x ∈ IOC∪IDC : <x,S(owl:DeprecatedClass)>∈ER(rdf:type) }
CEXT_I(S_I(owl:DeprecatedProperty)) = { x ∈ IOOP∪IODP : <x,S(owl:DeprecatedProperty)>∈ER(rdf:type) }
EXT_I(S_I(owl:DeprecatedClass)) = EXT_I(S_I(owl:DeprecatedProperty)) = {}

Then I is an OWL DL interpretation because the conditions for the class extensions in OWL DL match up with the conditions for class-like OWL abstract syntax constructs.

V', V, I', and I meet the requirements of Lemma 2, so for any directive D over V' I satisfies T(D) iff I' satisfies D.

Because O is imports closed, O includes all the ontologies that would be imported in T(O) the importing part of imports directives will be handled the same. Satisfying an abstract ontology is just satisfying its directives and satisfying the translation of an abstract ontology is just satisfying all the triples so I OWL DL satisfies T(K) iff I' direct satisfies K.

A.1.5 Correspondence Theorem

Theorem 1: Let O and O' be collections of OWL DL ontologies and axioms and facts in abstract syntax form that are imports closed, such that their union has a separated vocabulary, V', and every URI reference in V' is used in O. Then O entails O' if and only if T(O) OWL DL entails T(O').

Then I satisfies T(V'), because each URI reference in V' is used on O.

Proof: Suppose O entails O'. Let I be an OWL DL interpretation that satisfies T(O). Then from Lemma 3, there is some direct interpretation I' such that for any abstract OWL ontology or axiom or fact X over V', I satisfies T(X) iff I' satisfies X. Thus I' satisfies each ontology in O. Because O entails O', I' satisfies O', so I satisfies T(O'). Thus T(K),T(V') OWL DL entails T(Q).

Suppose T(O) OWL DL entails T(O'). Let I' be an direct interpretation that satisfies K. Then from Lemma 4, there is some OWL DL interpretation I such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I satisfies T(O). Because T(O) OWL DL entails T(O'), I satisfies T(O'), so I' satisfies O'. Thus O entails O'.

A.2 Correspondence between OWL DL and OWL Full

This section contains a proof sketch concerning the relationship between OWL DL and OWL Full. This proof has not been fully worked out. Significant effort may be required to finish the proof and some details of the relationship may have to change.

Let K be an RDF graph. An OWL interpretation of K is an OWL interpretation (from Section 5.2) that is an D-interpretation of K.

Lemma 5: Let V be a separated vocabulary. Then for every OWL intepretation I there is an OWL DL interpretation I' (as in Section 5.3) such that for K any OWL ontology in the abstract syntax with separated vocabulary V, I is an OWL interpretation of T(K) iff I' is an OWL DL interpretation of T(K).

Proof sketch: As all OWL DL interpretations are OWL interpretations, the reverse direction is obvious.

Let I = < R_I, EXT_I, S_I, L_I > be an OWL interpretation that satisfies T(K). Let I' = < R_I', EXT_I', S_I', L_I' > be an OWL interpretation that satisfies T(K). Let R_I' = CEXT_I(I(owl:Thing)) + CEXT_I(I(owl:ObjectProperty)) + CEXT_I(I(owl:ObjectProperty)) + CEXT_I(I(owl:Class)) + CEXT_I(I(rdf:List)) + R_I, where + is disjoint union. Define EXT_I' so as to separate the various roles of the copies. Define S_I' so as to map vocabulary into the appropriate copy. This works because K has a separated vocabulary, so I can be split according the the roles, and there are no inappropriate relationships in EXT_I. In essence the first component of R_I' is OWL individuals, the second component of R_I' is OWL datatype properties, the third component of R_I' is OWL individual-valued properties, the fourth component of R_I' is OWL classes, the fifth component of R_I' is RDF lists, and the sixth component of R_I' is everything else.

Theorem 2: Let O and O' be collections of OWL DL ontologies and axioms and facts in abstract syntax form that are imports closed, such that their union has a separated vocabulary (Section 4.2). Then the translation of O OWL Full entails the translation of O' if the translation of O OWL DL entails the translation of O'.

Proof: From the above lemma and because all OWL Full interpretations are OWL interpretations.

Note: The only if direction is not true.

OWL Web Ontology LanguageSemantics and Abstract Syntax Appendix A. Proofs (Informative)

Contents

Appendix A. Proofs (Informative)

A.1 Correspondence between Abstract OWL and OWL DL

A.1.1 Correspondence for Descriptions

A.1.2 Correspondence for Directives

A.1.3 From RDF Semantics to Direct Semantics

A.1.4 From Direct Semantics to RDF Semantics

A.1.5 Correspondence Theorem

A.2 Correspondence between OWL DL and OWL Full

OWL Web Ontology Language
Semantics and Abstract Syntax
Appendix A. Proofs (Informative)