Web Ontology Language (OWL) Abstract Syntax and Semantics
Appendix A. Correspondence between Abstract OWL and OWL/DL (Informative)

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

A.1 Correspondence between Abstract Syntax and OWL/DL
- A.1.1 Lemma 1
- A.1.2 Lemma 2
- A.1.3 Lemma 3
- A.1.4 Lemma 4
- A.1.5 Correspondence Theorem
A.2 Correspondence between OWL/DL and OWL/Full

Appendix A. Proofs (Informative)

This appendix contains proofs of theorems contained in the document.

A.1 Correspondence between Abstract OWL and OWL/DL

This section shows that the two semantics for OWL/DL correspond on certain OWL knowledge bases. One semantics used in this section is the direct model theory for abstract OWL knowledge bases 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 elements of their class extension.
Throughout this section T will be the mapping from OWL abstract knowledge bases to n-triples.

A separated OWL vocabulary is a set of URI references V with a disjoint partition 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 set of n-triples that contains exactly <v,rdf:type,owl:Thing > for v ∈ VI, <v,rdf:type,owl:Class > for v ∈ VC, <v,rdf:type,owl: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 knowledge bases 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.

A.1.1 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,S,EC,ER> be an abstract OWL interpretation over V'.
Let I = <R_I,S_I,EXT_I> be an OWL/DL interpretation over V of T(V'). Let CEXT_I have its usual meaning.
If R=CEXT_I(S_I(owl:Thing)), S(v)=S_I(v) for v ∈ VI, EC(v)=CEXT_I(S_I(v)) for v∈VC∪VD, and ER(v)=EXT_I(S_I(v)) for v∈VOP∪VDP
then for d any abstract OWL description or data range over V', I OWL/DL satisfies T(d) and
for any E mapping all the blank nodes of T(d) into R_I where I+E OWL/DL satisfies T(d),

CEXT_I(S_I(M(T(d)))) = EC(d),
if d is a description then S_I(M(T(d)))∈CEXT_I(S_I(owl:Class)), and
if d is a data range then S_I(M(T(d)))∈CEXT_I(S_I(owl:Datatype)).

Proof

The proof of the lemma is by a structural induction. Throughout the proof, let IOT = CEXT_I(S_I(owl:Thing)), IOC = CEXT_I(S_I(owl:Class)), IDC = CEXT_I(S_I(owl:Datatype)), IOOP = CEXT_I(S_I(owl:ObjectProperty)), IODP = CEXT_I(S_I(owl:DatatypeProperty)), and IL = CEXT_I(S_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 the n-triples of T(d) contains n-triples for each of the sub-constructs that do not share any blank nodes with n-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,S_I(owl:Thing)>∈EXT_I(S_I(rdfs:domain)) and <p,S_I(owl:Thing)>∈EXT_I(S_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 S_I(v)∈CEXT_I(S_I(owl:Class)). Because I is an OWL/DL interpretation CEXT_I(S_I(v))⊆IOT, so <S_I(v),S_I(owl:Thing)>∈EXT_I(S_I(rdfs:subClassOf)). Thus I OWL/DL satisfies T(v). As M(T(v)) is v, thus CEXT_I(S_I(M(T(v))))=EC(v). Finally, from above, S_I(v)∈IOC.
Base Case: v ∈ VD, including rdfs:Literal: As v∈VD and I satisfies T(V), thus S_I(v)∈CEXT_I(S_I(owl:Datatype)). Because I is an OWL/DL interpretation CEXT_I(S_I(v))⊆LV, so <S_I(v),S_I(rdfs:Literal)>∈EXT_I(S_I(rdfs:subClassOf)). Thus I OWL/DL satisfies T(v). As M(T(v)) is v, thus CEXT_I(S_I(M(T(v))))=EC(v). Finally, from above S_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 S_I(i_j)∈IOT. The second comprehension principle for sequences then requires that there is some l∈IL that is a sequence of S_I(i₁),…,S_I(i_n) over IOT. For any l that is a sequence of S_I(i₁),…,S_I(i_n) over IOT the comprehension principle for oneOf requires that there is some y∈CEXT_I(S_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+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = {S_I(i₁),…,S_I(i_n)} = EC(d). Finally, I+E(M(T(d)))∈IOC.
Base Case: d=oneOf(v₁…v_n), where the vi are typed data values: As v_j is a typed data value for 1≤j≤n S_I(v_j)∈LV. The second comprehension principle for sequences then requires that there is some l∈IL that is a sequence of S_I(v₁),…,S_I(v_n) over LV. For any l that is a sequence of S_I(v₁),…,S_I(v_n) over LV the comprehension principle for oneOf requires that there is some y∈CEXT_I(S_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+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = {S_I(i₁),…,S_I(i_n)} = EC(d). Finally, I+E(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'), S_I(p)∈IOOP∪IODP. As i∈VI and I satisfies T(V'), S_I(i)∈IOT. From a comprehension principle for restriction, I satisfies T(d). For any E such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = { x∈IOT | <x,S_I(i)> ∈ EXT_I(p) } = { x∈R | <x,S(i)> ∈ ER(p) } = EC(d). Finally, I+E(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 any extension of I, I+E, that satisfies T(d') has has I+E(M(T(d'))) = EC(d') and I+E(M(T(d')))∈IOC. The comprehension principle for complementOf then requires that there is a y∈IOC such that I+E satisfies <y,e>∈EXT_I(S_I(owl:complementOf)) so I satisfies T(d). For any I+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = IOT-CEXT_I(I+E(M(T(d)))) = R-EC(d') = EC(d). Finally, I+E(M(T(d)))∈IOC.
Inductive Case: d = unionOf(d₁ … d_n): From the induction hypothesis, I satisfies d_i for ₁≤i≤n so there is an extension of I, E_i, that maps all the blank nodes in T(d_i) into domain elements such that I+E_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+E₁+…+E_n, and thus I, satisfies T(d_i)∪…∪T(d_n). Each d_i is a description, so from the induction hypothesis, I+E₁+…+E_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+E₁+…+E_n(M(T(d₁))),…, I+E₁+…+E_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(S_I(owl:unionOf)) so I satisfies T(d).
For any I+E that satisfies T(d), I+E satisfies T(d_i) so CEXT_I(I+E(d_i)) = EC(d_i)). Then CEXT_I(I+E(M(T(d)))) = CEXT_I(I+E(d₁))∪…∪CEXT_I(I+E(d_n)) = EC(d₁)∪…∪EC(d_n) = EC(d). Finally, S_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 ₁≤i≤n so there is an extension of I, E_i, that maps all the blank nodes in T(restriction(p x_i)) into domain elements such that I+E_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+E₁+…+E_n, and thus I, satisfies T(restriction(p x₁))∩…∩T(restriction(p 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+E₁+…+E_n(M(T(restriction(p x_i))),…, I+E₁+…+E_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(S_I(owl:intersectionOf)) so I satisfies T(d).
For any I+E that satisfies T(d) I+E satisfies T(d_i) so CEXT_I(I+E(d_i)) = EC(d_i)). Then CEXT_I(I+E(M(T(d)))) = CEXT_I(I+E(restriction(p x_i)))∩…∩ CEXT_I(I+E(restriction(p x_n))) = EC(restriction(p x_i))cup;…∪EC(restriction(p x_i)) = EC(d). Finally, S_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 extension of I, I+E, that satisfies T(d') has I+E(M(T(d'))) = EC(d') and I+E(M(T(d')))∈IOC. As p∈VOP∪VDP and I satisfies T(V'), S_I(p)∈IOOP∪IODP. A comprehension principle for restriction then requires that I satisfies the n-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+E that satisfies T(d), CEXT_I(I+E(M(T(d)))) = {x∈IOT | ∀ y∈IOT : <x,y>∈EXT_I(p) → y∈CEXT_I(M(T(d')))} = {x∈R | ∀ y∈R : <x,y>∈ER(p) → y∈EC(d')} = EC(d). Finally, I+E(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.

A.1.2 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

Case: D = 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 E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d). Thus for some E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d) and I+E(M(T(d))∈IOC.

If I' satisfies D then EC(foo) = EC(d). From above, there is some E such that CEXT_I(I+E(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(S_I(foo)) and I+E(M(T(d))∈IOC. Because I satisfies T(V), S_I(foo))∈IOC, thus <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(owl:sameClassAs)). Therefore I satisfies T(D).

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

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

If I' satisfies D then EC(foo) ⊆ EC(d) From above, there is some E such that CEXT_I(I+E(M(T(d)))) = EC(d) ⊇ EC(foo) = CEXT_I(S_I(foo)) and I+E(M(T(d))∈IOC. Because I satisfies T(V), S_I(foo))∈IOC, thus <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(rdfs:subClassOf)). Therefore I satisfies T(D).

If I satisfies T(D) then I satisfies T(intersectionOf(d₁ … d_n)). Thus there is some E as above such that <S_I(foo),I+E(M(T(d)))> ∈ EXT_I(S_I(rdfs:subClassOf)). Thus EC(d) = CEXT_I(I+E(M(T(d)))) ⊇ CEXT_I(S_I(foo)) = EC(foo). Therefore I' satisfies D.

Case: D = 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 E mapping the blank nodes of T(d) such that I+E satisfies T(d), CEXT_I(I+E(M(T(d)))) = EC(d).

Case: D= DisjointClasses(d₁ … d_n)

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

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

If I' satisfies D then EC(d_i)∪EC(d_j) = {} for i≠j. For any E_i and E_j as above <I+E_i+E_j(M(T(d_i))),I+E_i+E_j(M(T(d_j)))< ∈ EXT_I(S_I(owl:disjointWith)), for i≠j. As at least one E_i exists for each i, and the blank nodes of the T(d_j) are all disjoint, I+E₁+…+E_n satisfies T(DisjointClasses(d₁ … d_n)). Therefore I satisfies T(D).

Case: D = EquivalentClasses(d₁ … d_n)

Similar.

Case: D = SubClassOf(d₁ d2)

Somewhat similar.

Case: D = IndividualProperty(p super(s₁) … super(sn) domain(d₁) … domain(d_m) range(r₁) … range(r_l) [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 E mapping the blank nodes of T(d_i) such that I+E satisfies T(d_i), CEXT_I(I+E(M(T(d_i)))) = EC(d_i). Similarly for r_i for 1≤i≤l.

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

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>∈EXT_I(p) iff <v,u>∈EXT_I(i) and I satisfies <S_I(p),S_I(i)>∈EXT_I(S_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> ∈ EXT_I(p) then <y, x>∈EXT_I(p). and thus I satisfies p∈CEXT_I(S_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, <S_I(p),S_I(s_i)>∈EXT_I(S_I(rdfs:subPropertyOf)). so ER(p)=EXT_I(S_I(p)) ⊆ EXT_I(S_I(s_i))=ER(s_i). Also, for 1≤i≤m, for some E such that I+E satisfies T(d_i), <S_I(p),I+E(M(T(d_i)))>∈EXT_I(S_I(rdfs:domain)) so <z,w>∈EXT_I(p) → z∈CEXT_I(I+E(M(T(d_i)))). Thus <z,w>∈ER(p) → z∈EC(d_i) and ER(p)⊆EC(d_i)×R. Similarly for r_i) for 1≤i≤l.

If I satisfies T(D) and inverse(i) is in D, then I satisfies <S_I(p),S_I(i)>∈EXT_I(S_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 D and Symmetric is in D, then I satisfies p∈CEXT_I(S_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(D) then I' satisfies D.

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

Similar.

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

As p_i∈VOP and I satisfies T(V'), S_I(p_i)∈IOP. If I satisfies T(D) then <S_I(p_i),S_I(p_j)> ∈ EXT_I(S_I(owl:samePropertyAs)), for each 1≤i<j≤n. Therefore EXT_I(p_i) = EXT_I(p_j), for each 1≤i<j≤n; CR(p_i) = CR(p_j), for each 1≤i<j≤n; and I' satisfies D.

If I' satisfies D then CR(p_i) = CR(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:samePropertyAs, <S_I(p_i),S_I(p_j)> ∈ EXT_I(S_I(owl:samePropertyAs)), for each 1≤i<j≤n. Thus I satisfies T(D).

Case: D = SubPropertyOf(p₁ p₂)

Somewhat similar, but simpler.

Case: D = SameIndividual(i₁ … i_n)

Similar to SamePropertyAs.

Case: D = DifferentIndividuals(i₁ … i_n)

Similar to SamePropertyAs.

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

If I satisfies T(D) then there is some E that maps each blank node in T(D) such that I+E satisfies T(D). A simple examination of T(D) shows that the mappings of E 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 class memberships and relationships true in D. The n-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).

A.1.3 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 = < R_I, EXT_I, S_I > over V that satisfies T(V') there is an abstract OWL interpretation I' over V' such that for any OWL abstract KB K over V, I' abstract OWL satisfies K iff I OWL/DL satisfies T(K).

Proof

Let CEXT_I be defined as usual from I. The required abstract OWL interpretation will be I' = < CEXT_I(S_I(owl:Thing)), S, EC, ER > where S(n) = S_I(n) for n∈VI, EC(n) = CEXT_I(S_I(n)) for n∈VC∪VD, and ER(n) = EXT_I(S_I(n)) for n∈VOP∪VDP.
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.
Satisfying an abstract KB is just satisfying its directives and satisfying the translation of an abstract KB is just satisfying all the n-triples so I OWL/DL satisfies T(K) iff I' abstract OWL satisfies K.

A.1.4 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, S, EC, ER > over V' there is an OWL/DL interpretation I over V that satisfies T(V') such that for any abstract OWL KB K over V', I OWL/DL satisfies T(K) iff I' abstract OWL satisfies K.

Proof

Construct I = < R_I, EXT_I, S_I > as follows:
- Let IOC be the OWL descriptions over V', i.e., C is part of the Herbrand universe of OWL syntax.
  Let OD be the OWL data ranges over V'.
  Let OP = VOP u VDP.
  Let OL be the finite sequences over U, over C, and over LV plus rdf:nil.
  Let OX = VRDFS∪VOWL - {rdf:nil}.
- R_I = U ∪ IOC ∪ OD ∪ OP ∪ OL ∪ OX
- Let S_I(n) = S(n) for n∈VI.
  Let S_I(n) = n for n∈V-VI.
- For i∈U, EXT_I(i)={} and CEXT_I(i)={}.
  For c∈IOC, EXT_I(c)={} and CEXT_I(c)=EC(c).
  For d∈OD, EXT_I(d)={} and CEXT_I(d)=EC(d).
  For r∈OP, EXT_I(r)=ER(r) and CEXT_I(r)={}.
  For l∈OL, EXT_I(r)={} and CEXT_I(r)={}.
- CEXT_I(rdf:first)={}, CEXT_I(rdf:rest)={}
  CEXT_I(rdf:nil)={}, EXT_I(rdf:nil)={}
  CEXT_I(rdf:List)=OL, EXT_I(rdf:List)={}
  <x,y> ∈ EXT_I(rdf:first) iff x∈OL and y is its first element
  <x,y> ∈ EXT_I(rdf:rest) iff x∈OL and y is its tail
- owl:intersectionOf, owl:oneOf, owl:unionOf, owl:complementOf, owl:onProperty, owl:allValuesFrom, owl:someValuesFrom, owl:hasValue, owl:minCardinality, owl:maxCardinality, and owl:cardinality have empty class extensions and their extensions are as necessary to link the elements of IOC up with their parts.
CEXT_I(rdfs:range) = {};
EXT_I(rdfs:range) = { <x,y> : x∈OP y∈IOC ∧ ∀ z, <w,z> ∈ EXT_I(x) → z ∈ CEXT_I(y); } ∪ [RDFS ranges]
CEXT_I(rdfs:subClassOf) = {};
EXT_I(rdfs:subClassOf) = { <x,y> : x,y∈IOC ∧ CEXT_I(x) ⊆ CEXT_I(y) } ∪ [RDFS subclasses]
CEXT_I(rdfs:subPropertyOf) = {};
EXT_I(rdfs:subPropertyOf) = { <x,y> : x,y∈OP ∧ EXT_I(x) ⊆ EXT_I(y) } ∪ [RDFS subproperties]
CEXT_I(rdf:type) = {}, EXT_I(rdf:type) is determined by CEXT_I. 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.
Satisfying an abstract KB is just satisfying its directives and satisfying the translation of an abstract KB is just satisfying all the n-triples so I OWL/DL satisfies T(K) iff I' abstract OWL satisfies K.

A.1.5 Correspondence Theorem

Let V' be a separated OWL vocabulary. Let K,Q be abstract OWL knowledge bases 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 knowledge base 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 knowledge base 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.

A.2 Correspondence between OWL/DL and OWL/Full

This section contains a poof 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 a collection of n-triples. An OWL interpretation of of K is an OWL interpretation (from Section 5.2) that is an RDFS interpretation of K.

Lemma: Let K be an OWL KB in the abstract syntax with separated vocabulary. Then for every OWL interpretation of T(K) there is an OWL/DL interpretation (as in Section 5.3) of T(K), and vice versa.

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

Let I = < R_I, EXT_I, S_I > be an OWL interpretation of T(K). Let I' = < R_I', EXT_I', S_I' > be an OWL interpretation of T(K). Let R_I' = CEXT_I(S_I(owl:Thing)) + CEXT_I(S_I(owl:ObjectProperty)) + CEXT_I(S_I(owl:IndividualProperty)) + CEXT_I(S_I(owl:Class)) + CEXT_I(S_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 S_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: Let K,C be collections of n-triples 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.

Web Ontology Language (OWL) Abstract Syntax and Semantics Appendix A. Correspondence between Abstract OWL and OWL/DL (Informative)

Contents

Appendix A. Proofs (Informative)

A.1 Correspondence between Abstract OWL and OWL/DL

A.1.1 Lemma 1

A.1.2 Lemma 2

A.1.3 Lemma 3

A.1.4 Lemma 4

A.1.5 Correspondence Theorem

A.2 Correspondence between OWL/DL and OWL/Full

Web Ontology Language (OWL) Abstract Syntax and Semantics
Appendix A. Correspondence between Abstract OWL and OWL/DL (Informative)