Copyright ©2002 W3C © ( MIT, INRIA, 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 for OWL DL correspond on certain OWL ontologies. One semantics used in this section is the direct model theory for abstract OWL ontologies given in the direct model-theoretic semantics section of this document. The other semantics is the extension of the RDFS semantics given in the RDFS-compatible model-theoretic semantics section of this document.
Throughout this section qualified names are used as shorthand for URI
references.
The namespace identifiers used in such names, namely rdf, rdfs, xsd,
and owl, should be used as if they are given their usual definitions.
Throughout this section
VRDFS is the RDF and RDFS built-in vocabulary,
i.e., rdf:type, rdf:Property, rdfs:Class, rdfs:subClassOf, …,
minus rdfs:Literal; and
VOWL is the OWL built-in vocabulary,
i.e., owl:Class, owl:onProperty, …,
minus owl:Thing and owl:Nothing.
Throughout this section D will be a datatyping scheme, i.e., a set of
URI references that have class extensions that are subsets of LV and
mappings from strings to their class extension.
Throughout this section T will be the mapping from abstract OWL
ontologies to RDF graphs.
Recall that a separated OWL vocabulary is a set of URI references V with a disjoint partition, written V = VI + VC + VD + VOP + VDP where owl:Thing and owl:Nothing are in VC, rdfs:Literal is in VD, and all the elements of D are in VD. Further V is disjoint from VRDFS∪VOWL.
An OWL abstract KB with separated names over a separated OWL vocabulary V = VI + VC + VD + VOP + VDP is a set of OWL axioms and facts without annotations as in Section 2 where <individualID>s are taken from VI, <classID>s are taken from VC, <datatypeID>s are taken from VD, <individualvaluedPropertyIDs> are taken from VOP, and <datavaluedPropertyID>s are taken from VDP.
Let V = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Then T(V) is the RDF graph that contains exactly <v,rdf:type,owl:Thing > for v ∈ VI, <v,rdf:type,owl:Class > for v ∈ VC, <v,rdf:type,rdfs:Datatype > for v ∈ VD, <v,rdf:type,owl:ObjectProperty > for v ∈ VOP, and <v,rdf:type,owl:DatatypeProperty > for v ∈ VDP.
The theorem to be proved is:
Let V' be a separated OWL vocabulary.
Let K,Q be abstract OWL ontologies with separated names over V'.
Then K OWL entails Q iff T(K),T(V') OWL DL entails T(Q).
Actually, a slightly stronger correspondence can be shown, but this is enough for now, as the presence of annotations and imports causes even more complications.
Lemma 1:
Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary.
Let V = VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VRDFS ∪ VOWL.
Let I'= <R,EC,ER,S> be an abstract OWL interpretation of V'.
Let I = <RI,PI,EXTI,SI,LI>
be an OWL DL interpretation of V that satisfies T(V').
Let CEXTI have its usual meaning, and, as usual, overload I to
map any syntactic construct into its denotation.
If R=CEXTI(I(owl:Thing)),
S(v)=SI(v) for v ∈ VI,
EC(v)=CEXTI(SI(v)) for v∈VC∪VD, and
ER(v)=EXTI(SI(v)) for v∈VOP∪VDP
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 = CEXTI(I(owl:Thing)), IOC = CEXTI(I(owl:Class)), IDC = CEXTI(I(rdfs:Datatype)), IOOP = CEXTI(I(owl:ObjectProperty)), IODP = CEXTI(I(owl:DatatypeProperty)), and IL = CEXTI(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)>∈EXTI(I(rdfs:domain)) and <p,I(owl:Thing)>∈EXTI(I(rdfs:range)). Thus I satisfies T(p). Similarly for p∈VDP.
Lemma 2: Let V', V, I', and I be as in Lemma 1. Let D be an OWL directive over V'. Then I satisfies T(D) iff I' satisfies D.
Proof
Let d=intersectionOf(d1 … dn). 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), CEXTI(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), CEXTI(I+A(M(T(d)))) = EC(d) and I+A(M(T(d))∈IOC.
If I' satisfies D then EC(foo) = EC(d). From above, there is some A such that CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(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)))> ∈ EXTI(I(owl:sameClassAs)). Therefore I satisfies T(D).
If I satisfies T(D) then I satisfies T(intersectionOf(d1 … dn)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:sameClassAs)). Thus EC(d) = CEXTI(I+A(M(T(d)))) = CEXTI(I(foo)) = EC(foo). Therefore I' satisfies D.
Let d=intersectionOf(d1 … dn). 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), CEXTI(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), CEXTI(I+A(M(T(d)))) = EC(d) and I+A(M(T(d))∈IOC.
If I' satisfies D then EC(foo) ⊆ EC(d). From above, there is some A such that CEXTI(I+A(M(T(d)))) = EC(d) ⊇ EC(foo) = CEXTI(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)))> ∈ EXTI(I(rdfs:subClassOf)). Therefore I satisfies T(D).
If I satisfies T(D) then I satisfies T(intersectionOf(d1 … dn)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXTI(I(rdfs:subClassOf)). Thus EC(d) = CEXTI(I+A(M(T(d)))) ⊇ CEXTI(I(foo)) = EC(foo). Therefore I' satisfies D.
Let d=oneOf(i1 … in). 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), CEXTI(I+A(M(T(d)))) = EC(d).
If I' satisfies D then EC(foo) = EC(d). From above, there is some A such that CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(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)))> ∈ EXTI(I(owl:sameClassAs)). Therefore I satisfies T(D).
If I satisfies T(D) then I satisfies T(intersectionOf(d1 … dn)). Thus there is some A as above such that <I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:sameClassAs)). Thus EC(d) = CEXTI(I+A(M(T(d)))) = CEXTI(I(foo)) = EC(foo). Therefore I' satisfies D.
As di is a description over V' therefore I satisfies T(di) and for any A mapping the blank nodes of T(di) such that I+A satisfies T(di), CEXTI(I+A(M(T(di)))) = EC(di).
If I satisfies T(D) then for 1≤i≤n there is some Ai such that I satisfies <I+Ai(M(T(di))),I+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith)) for each 1≤i<j≤n. Thus EC(di)∩EC(dj) = {}, for i≠j. Therefore I' satisfies D.
If I' satisfies D then EC(di)∩EC(dj) = {} for i≠j. For any Ai and Aj as above <I+Ai+Aj(M(T(di))),I+Ai+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith)), for i≠j. As at least one Ai exists for each i, and the blank nodes of the T(dj) are all disjoint, I+A1+…+An satisfies T(DisjointClasses(d1 … dn)). Therefore I satisfies T(D).
As di for 1≤i≤m is a description over V' therefore I satisfies T(di) and for any A mapping the blank nodes of T(di) such that I+A satisfies T(di), CEXTI(I+A(M(T(di)))) = EC(di). Similarly for ri for 1≤i≤k.
If I' satisfies D, then, as p∈VOP, I satisfies I(p)∈IOOP. Then, as I is an OWL DL interpretation, I satisfies <I(p),I(owl:Thing)>∈EXTI(I(rdfs:domain)) and <I(p),I(owl:Thing)>∈EXTI(I(rdfs:range)). Also, ER(p)⊆ER(si) for 1≤i≤n, so EXTI(I(p))=ER(p) ⊆ ER(si)=EXTI(I(si)) and I satisfies <I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf)). Next, ER(p)⊆EC(di)×R for 1≤i≤m, so <z,w>∈ER(p) → z∈EC(di) and for any A such that I+A satisfies T(di), <z,w>∈EXTI(p) → z∈CEXTI(I+A(M(T(di)))) and thus <I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain)). Similarly for ri for 1≤i≤k.
If I' satisfies D and inverse(i) is in D, then ER(p) and ER(i) are converses. Thus <u,v>∈ER(p) iff <v,u>∈ER(i) so <u,v>∈EXTI(p) iff <v,u>∈EXTI(i) and I satisfies <I(p),I(i)>∈EXTI(I(owl:inverseOf)). If I' satisfies D and Symmetric is in D, then ER(p) is symmetric. Thus if <x,y>∈ ER(p) then <y,x>∈ER(p) so if <x,y> ∈ EXTI(p) then <y, x>∈EXTI(p). and thus I satisfies p∈CEXTI(I(owl:Symmetric)). Similarly for Functional, InverseFunctional, and Transitive. Thus if I' satisfies D then I satisfies T(D).
If I satisfies T(D) then, for 1≤i≤n, <I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf)) so ER(p)=EXTI(I(p)) ⊆ EXTI(I(si))=ER(si). Also, for 1≤i≤m, for some A such that I+A satisfies T(di), <I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain)) so <z,w>∈EXTI(p) → z∈CEXTI(I+A(M(T(di)))). Thus <z,w>∈ER(p) → z∈EC(di) and ER(p)⊆EC(di)×R. Similarly for ri for 1≤i≤k.
If I satisfies T(D) and inverse(i) is in D, then I satisfies <I(p),I(i)>∈EXTI(I(owl:inverseOf)). Thus <u,v>∈EXTI(p) iff <v,u>∈EXTI(i) so <u,v>∈ER(p) iff <v,u>∈ER(i) and ER(p) and ER(i) are converses. If I satisfies D and Symmetric is in D, then I satisfies p∈CEXTI(I(owl:Symmetric)) so if <x,y> ∈ EXTI(p) then <y, x>∈EXTI(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(D) then I' satisfies D.
As pi∈VOP and I satisfies T(V'), I(pi)∈IOP. If I satisfies T(D) then <I(pi),I(pj)> ∈ EXTI(I(owl:samePropertyAs)), for each 1≤i<j≤n. Therefore EXTI(pi) = EXTI(pj), for each 1≤i<j≤n; ER(pi) = ER(pj), for each 1≤i<j≤n; and I' satisfies D.
If I' satisfies D then ER(pi) = ER(pj), for each 1≤i<j≤n. Therefore EXTI(pi) = EXTI(pj), for each 1≤i<j≤n. From the OWL DL definition of owl:samePropertyAs, <I(pi),I(pj)> ∈ EXTI(I(owl:samePropertyAs)), for each 1≤i<j≤n. Thus I satisfies T(D).
If I satisfies T(D) then there is some A that maps each blank node in T(D) such that I+A satisfies T(D). A simple examination of T(D) shows that the mappings of A plus the mappings for the individual IDs in D, which are all in IOT, show that I' satisfies D.
If I' satisfies D then for each Individual construct in D there must be some element of R that makes the type relationships and relationships true in D. The triples in T(D) 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(D).
Lemma 3: Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Let V = VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VRDFS ∪ VOWL. Then for every OWL DL interpretation I = < RI, PI, EXTI, SI, LI > of V that satisfies T(V') there is an abstract OWL interpretation I' of V' such that for any OWL abstract KB K of V, I' abstract OWL satisfies K iff I OWL DL satisfies T(K).
Proof
Let CEXTI be defined as usual from I. The required abstract OWL interpretation will be I' = < CEXTI(I(owl:Thing)), EC, ER, S > where S(n) = I(n) for n∈VI, EC(n) = CEXTI(I(n)) for n∈VC∪VD, and ER(n) = EXTI(I(n)) for n∈VOP∪VDP.
Satisfying an abstract KB is just satisfying its directives and satisfying the translation of an abstract KB is just satisfying all the triples so I OWL DL satisfies T(K) iff I' abstract OWL satisfies K.
Lemma 4: Let V' = VI + VC + VD + VOP + VDP be a separated OWL vocabulary. Let V = VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VRDFS ∪ VOWL. Then for every Abstract OWL interpretation I' = < U, EC, ER, S > of V' there is an OWL DL interpretation I of V that satisfies T(V') such that for any abstract OWL KB K of V', I OWL DL satisfies T(K) iff I' abstract OWL satisfies K.
Proof
Theorem 1: Let V' be a separated OWL vocabulary. Let K,Q be abstract OWL ontologies with separated names over V'. Then K OWL entails Q iff T(K),T(V') OWL DL entails T(Q).
Proof
Suppose K OWL entails Q. Let I be an OWL DL interpretation that satisfies T(K),T(V'). Then from Lemma 3, there is some abstract OWL interpretation I' such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I' satisfies K. Because K OWL entails Q, I' satisfies Q, so I satisfies T(Q). Thus T(K),T(V') OWL DL entails T(Q).
Suppose T(K),T(V') OWL DL entails T(Q). Let I' be an abstract OWL interpretation that satisfies K. Then from Lemma 4, there is some OWL DL interpretation I that satisfies T(V') such that for any abstract OWL ontology X over V', I satisfies T(X) iff I' satisfies X. Thus I satisfies T(K). Because T(K),T(V') OWL DL entails T(Q), I satisfies T(Q), so I' satisfies Q. Thus K abstract OWL entails Q.
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 RDFS 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 KB 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 = < RI, EXTI, SI, LI > be an OWL interpretation that satisfies T(K). Let I' = < RI', EXTI', SI', LI' > be an OWL interpretation that satisfies T(K). Let RI' = CEXTI(I(owl:Thing)) + CEXTI(I(owl:ObjectProperty)) + CEXTI(I(owl:IndividualProperty)) + CEXTI(I(owl:Class)) + CEXTI(I(rdf:List)) + RI, where + is disjoint union. Define EXTI' so as to separate the various roles of the copies. Define SI' 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 EXTI. In essence the first component of RI' is OWL individuals, the second component of RI' is OWL datatype properties, the third component of RI' is OWL object properties, the fourth component of RI' is OWL classes, the fifth component of RI' is RDF lists, and the sixth component of RI' is everything else.
Theorem 2: Let K,C be RDF graphs such that each of K, C, and K∪C is the translation of some OWL KB in the abstract syntax with separated vocabulary. Then K OWL Full entails C if K OWL DL entails C.
Proof: From the above lemma and because all OWL Full interpretations are OWL interpretations.
Comment: The only if direction cannot be proved without showing that OWL Full has no semantic oddities, which has not yet been done.