Copyright © 2003 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark, document use and software licensing rules apply.
This appendix contains proofs of theorems contained in Section 5 of the document.
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.
Nomenclature: Throughout this section D will be a datatype theory (Section 3.1) containing datatypes for all the built-in OWL datatypes; 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.
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 for the and 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 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:
The theorem to be proved is then: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are consistent with the Web, such that their union has a separated vocabulary. Then O direct entails O' if and only if T(O) OWL DL entails T(O') the translation of the ontologies in O' (exending T to allow it to translate collections of ontologies in the obvious way).
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> 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_{D}. Let CEXT_{I} have its usual meaning, and, as usual, overload I to map any syntactic construct into its denotation. If
then for d any abstract OWL description or data range over V',
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.
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.
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 that have URI references as their objects, the lemma can be easily established by an inspection of the semantic condition and the translation triples. For annotations that have an Individual(…) as their object, 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 simlar fashion and will also be ignored in the rest of the proof.
Let d=intersectionOf(d_{1} … 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 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.
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)). Therefore I satisfies T(F).
If I satisfies T(F) then I satisfies T(intersectionOf(d_{1} … 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.
Let d=intersectionOf(d_{1} … 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 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.
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(rdfs:subClassOf)). Therefore I satisfies T(F).
If I satisfies T(F) then I satisfies T(intersectionOf(d_{1} … d_{n})). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXT_{I}(I(rdfs:subClassOf)). Thus EC(d) = CEXT_{I}(I+A(M(T(d)))) ⊇ CEXT_{I}(I(foo)) = EC(foo). Therefore I' satisfies F.
Let d=oneOf(i_{1} … 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), CEXT_{I}(I+A(M(T(d)))) = EC(d).
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)). Therefore I satisfies T(F).
If I satisfies T(F) then I satisfies T(intersectionOf(d_{1} … 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.
The only thing that needs to be shown here is the typing for foo, which is similar to that for classes.
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_{1}+…+A_{n} satisfies T(DisjointClasses(d_{1} … d_{n})). Therefore I satisfies T(F).
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.
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).
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).
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 O with vocabulary V' such that O is consistent with the Web, 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' = < CEXT_{I}(I(owl:Thing)), EC, ER, L, S > where
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 consistent with the web, 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.
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 > of V' there is an OWL DL interpretation I of V that satisfies T(V') such that for any collection of OWL abstract ontologies O with vocabulary V' such that O is consistent with the Web, 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:
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 consistent with the web, 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.
Theorem 1: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are consistent with the Web, 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') the translation of the ontologies in O' (exending T to allow it to translate collections of ontologies in the obvious way).
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 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'.
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:IndividualProperty)) + 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 object 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 in abstract syntax form that are consistent with the Web, such that their union has a separated vocabulary (Section 4.2). Then the translation of the ontologies in O OWL Full entails the translation of the ontologies in O' if the translation of the ontologies in O OWL DL entails the translation of the ontologies in O'.
Proof: From the above lemma and because all OWL Full interpretations are OWL interpretations.
Note: The only if direction cannot be proved without showing that OWL Full has no semantic oddities, which has not yet been done.