このドキュメントに対する正誤表を参照してください。いくつかの規範的な修正が含まれているかもしれません。
翻訳版も参照してください。
Copyright c 2004 W3CR (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark, document use and software licensing rules apply.
この付録には、ドキュメントの5項に含まれる定理の証明が含まれています。
名称: この付録の全体にわたって、Dは、すべての組み込みOWLデータ型およびrdf:XMLLiteralに対するデータ型を含むデータ型マップ(3.1項)で、Tは、4.1項の抽象OWLオントロジーからRDFグラフへのマッピングです。そして、VBは組み込みOWL語彙です。さらに、語彙中のプレーンなリテラルについては言及しません。
注: この付録の全体にわたって、すべての解釈は、データ型マップDに関するのもです。したがって、すべての結果はDに関するものです。構築に関する分かりきったことの詳細の一部は省略しています。
この項では、3項の抽象OWLオントロジーに対する直接モデル理論(ここでは、直接モデル理論と呼ばれる)および5項のOWL DLセマンティクス(ここでは、OWL DLモデル理論と呼ばれる)の2つのセマンティクスの、あるOWLオントロジーでの対応を紹介します。
定義: 上記のDに関しては、分離されたOWL語彙(4.2項)は、V' = VO + VC + VD + VI + VOP + VDP + VAP + VXPと記述される、V'の互いに素の分割を用いて、ここでさらに1組のURI参照V'(許されていない語彙(4.2項)と素の関係である)へ形式化され、ここでは、組み込みOWLクラスがVCにあり、Dとrdfs:Literalのすべてのデータ型名に対するURI参照がVDにあり、OWL組み込みアノテーション・プロパティーがVAPにあり、そして、 OWL組み込みオントロジー・プロパティーがVXPにあります。
定義: 分離されたOWL語彙の解釈V' = VO + VC + VD + VI + VOP + VDP + VAP + VXP(T(V')と記述)は、以下の形式のすべてのトリプルから成ります。
v rdf:type owl:Ontology(v ∈ VOに対し)、
v rdf:type owl:Class(v ∈ VCに対し)、
v rdf:type rdfs:Datatype(v ∈ VDに対し)、
v rdf:type owl:Thing(v ∈ VIに対し)、
v rdf:type owl:ObjectProperty(v ∈ VOPに対し)、
v rdf:type owl:DatatypeProperty(v ∈ VDPに対し)、
v rdf:type owl:AnnotationProperty(v ∈ VAPに対し)、および
v rdf:type owl:OntologyProperty(v ∈ VXPに対し)。
定義: 分離された語彙(4項)を持つ、抽象構文形式のOWL DLオントロジーのコレクションおよび公理と事実、0(2項)は、以下のように、ここでさらに分離された新しい概念の語彙V = VO + VC + VD + VI + VOP + VDP + VAP + VXPで形式化されます。
このとき、証明される定理は、OおよびO'を、それらの和集合が分離された語彙を持っているような、閉じたインポートである、抽象構文形式のOWL DLオントロジーのコレクションおよび公理と事実とします。このとき、T(O)がT(O')をOWL DL含意する場合に限り、OはO'を直接含意します。
補助定理1: V' = VO + VC + VD + VI + VOP + VDP + VAP + VXPを分離されたOWL語彙とします。V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪をVBとします。I'= <R,EC,ER,L,S,LV>をV'の直接解釈とします。LVI = LVであれば、I = <RI,PI,EXTI,SI,LI,LVI>をT(V')を満たすVのOWL DL解釈とします。CEXTIがその通常の意味を持っているものとし、かつ、いつものように、任意の構文構成子をその表示にマッピングするようにIをオーバーロード(overload)させます。もし、
である場合、任意の抽象OWL記述あるいはV'を超えるデータ値域である、dに対し、
証明:
補助定理の証明は、構造帰納法(structural induction)によります。証明の全体にわたって、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))、そしてIL = CEXTI(I(rdf:List))とします。
帰納法を機能させるためには、サブ構成子T(d)を持つ記述またはデータ値域である、任意のdに対し、他のサブ構成子からのトリプルといかなる空白ノードも共有しない、それぞれのサブ構成子に対するトリプルを含んでいることを示す必要があります。これは、Tの規則から容易に立証することができます。
p∈VOPである場合、Iはp∈IOOPを満たします。このとき、IはOWL DL解釈であるため、Iは<p,I(owl:Thing)>∈EXTI(I(rdfs:domain))および<p,I(owl:Thing)>∈EXTI(I(rdfs:range))を満たします。したがって、IはT(p)を満たします。p∈VDPの場合も同様です。
補助定理1.1: V'、V、I'、およびIを補助定理1と同様とします。dをV'上の抽象OWL個体構成子とします(Individual(…)形式の)。このとき、I+AがT(d)をOWL DLで満たす場合の、T(d)のすべての空白ノードをRIにマッピングする任意のAに対し、I+A(M(T(d))) ∈ EC(d)です。さらに、任意のr ∈ EC(d)に対し、I+A(M(T(d))) = rのような、T(d)のすべての空白ノードをRIにマッピングするAが存在します。
証明:
シンプルな帰納論証(inductive argument)は、I+A(M(T(d)))がEC(d)のすべての要件を満たさなければならないことを示します。別の帰納論証(サブ構成子における空白ノードの非共有性に依る)は、r ∈ EC(d)ごとに、I+A(M(T(d))) = rであるような、あるAが存在することを示します。
補助定理1.9: V'、V、I'、およびIを補助定理1と同様とします。Fをannotation(p x)形式のアノテーションを持つV'上のOWL命令とします。Fがクラスまたはプロパティー公理である場合、nをそのクラスあるいはプロパティーの名前とします。Fが個体の公理であれば、nをT(F)の主要ノードとします。このとき、T(F)のすべての空白ノードをRIにマッピングする任意のAに対し、I'がアノテーションによって生じる条件を直接満たす場合に限り、I+Aは、アノテーションによって生じるトリプルをOWL DLで満たします。
証明:
URI参照へのアノテーションに対し、セマンティック条件の検出および翻訳トリプルによって補助定理を容易に確立することができます。Individual(…)へのアノテーションに対し、補助定理1.1の使用も必要です。
補助定理2: V'、V、I'、およびIを補助定理1と同様とします。FをV'上のOWL命令とします。このとき、I'がFを満たす場合に限り、IはT(F)を満たします。
証明:
証明の主要部分は、命令上の構造帰納法(structural induction)です。アノテーションは、多くの命令に生じ、それが補助定理1.9の使用をちょうど要求するのと全く同じように動作します。したがって、残りの証明は、アノテーションを無視するでしょう。非推奨は、同様の方法で扱うことができ、これも残りの証明では無視されるでしょう。
d=intersectionOf(d1 … dn)とします。dはV'上の記述であるため、IはT(d)を満たし、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする任意のAに対し、CEXTI(I+A(M(T(d)))) = EC(d)です。したがって、dの任意のサブ記述であるd'に対し、CEXTI(I+A(M(T(d')))) = EC(d')、かつ、I+A(M(T(d')))∈IOCです。したがって、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする、あるAに対し、CEXTI(I+A(M(T(d)))) = EC(d)、かつ、I+A(M(T(d)))∈IOC、そして、dのサブ記述であるd'ごとに、CEXTI(I+A(M(T(d')))) = EC(d')、かつ、I+A(M(T(d')))∈IOCです。
I'がFを満たす場合、 EC(foo) = EC(d)です。以上から、CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(I(foo))、かつ、I+A(M(T(d)))∈IOCであるような、あるAが存在します。IはT(V)を満たすため、I(foo)∈IOCであり、したがって、<I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:equivalentClass))です。さらに、I(owl:intersectionOf)におけるセマンティック条件のために、<I(foo),I+A(M(T(SEQ d1 … dn)))> ∈ EXTI(I(owl:intersectionOf))です。
dが形式intersectionOf(d1)に属している場合、CEXTI(I+A(M(T(d1)))) = EC(d1) = EC(d) = EC(foo)、かつ、I+A(M(T(d1)))∈IOCです。よって、I(owl:equivalentClass)におけるセマンティック条件から、<I(foo),I+A(M(T(d1)))> ∈ EXTI(I(owl:equivalentClass))です。d1が形式complementOf(d'1)に属している場合、IOT - CEXTI(I+A(M(T(d'1)))) = CEXTI(I+A(M(T(d1)))) = EC(d1) = EC(d) = EC(foo)、かつ、I+A(M(T(d'1)))∈IOCです。よって、I(owl:complementOf)におけるセマンティック条件から、<I(foo),I+A(M(T(d'1)))> ∈ EXTI(I(owl:complementOf))です。d1が形式unionOf(d11 … d1m)に属している場合、CEXTI(I+A(M(T(d11)))) ∪ … ∪ CEXTI(I+A(M(T(d1m)))) = CEXTI(I+A(M(T(d1)))) = EC(d1) = EC(d) = EC(foo)、かつ、I+A(M(T(d1j)))∈IOCです(1≤ j ≤mに対し)。よって、I(owl:unionOf)におけるセマンティック条件から、<I(foo),I+A(M(T(SEQ d11 … d1m)))> ∈ EXTI(I(owl:unionOf))です。
したがって、IはT(F)を満たします(潜在的なT(F)ごとに)。
IがT(F)を満たす場合、IはT(intersectionOf(d1 … dn))を満たします。したがって、<I(foo),I+A(M(T(d)))> ∈ EXTI(I(owl:equivalentClass))であるような、上記のような、あるAが存在します。したがって、EC(d) = CEXTI(I+A(M(T(d)))) = CEXTI(I(foo)) = EC(foo)です。したがって、I' はFを満たします。
d=intersectionOf(d1 … dn)とします。dがV'上の記述であるため、IはT(d)を満たし、I+AがT(d)を満たすような、T(d)のブ空白ノードをマッピングする任意のAに対し、CEXTI(I+A(M(T(d)))) = EC(d)です。したがって、CEXTI(I+A(M(T(di)))) = EC(di)です(1 ≤ i ≤ nに対し)。したがって、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする、あるAに対し、CEXTI(I+A(M(T(di)))) = EC(di)、かつ、I+A(M(T(di))∈IOCです(1 ≤ i ≤ nに対し)。
I'がFを満たす場合、EC(foo) ⊆ EC(di)です(1 ≤ i ≤ nに対し)。以上から、CEXTI(I+A(M(T(di)))) = EC(di) ⊇ EC(foo) = CEXTI(I(foo))、かつ、I+A(M(T(di))∈IOCであるような、あるAが存在します。IがT(V)を満たすため、I(foo)∈IOCであり、したがって、<I(foo),I+A(M(T(di)))> ∈ EXTI(I(rdfs:subClassOf))です(1 ≤ i ≤ nに対し)。したがって、IはT(F)を満たします。
IがT(F)を満たす場合、IはT(di)を満たします(1 ≤ i ≤ nに対し)。したがって、<I(foo),I+A(M(T(di)))> ∈ EXTI(I(rdfs:subClassOf))(1 ≤ i ≤ nに対し)であるような、上記のような、あるAが存在します。したがって、EC(d) = CEXTI(I+A(M(T(di)))) ⊇ CEXTI(I(foo)) = EC(foo)です(1 ≤ i ≤ nに対し)。したがって、I' はFを満たします。
d=oneOf(i1 … in)とします。dがV'上の記述であるため、ゆえにIはT(d)を満たし、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする、あるAに対し、EC(d) = CEXTI(I+A(M(T(d)))) = {SI(M(T(i1)), … SI(M(T(in))}です。さらに、SI(M(T(ij)) ∈ IOTです(1 ≤ j ≤ nに対し)。
I'がFを満たす場合、EC(foo) = EC(d)です。以上から、CEXTI(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXTI(I(foo))、かつ、I+A(M(T(d))∈IOCである、あるAが存在します。eをI+A(M(T(SEQ i1 … in)))とします。このとき、I(owl:oneOf)におけるセマンティック条件から、<I(foo),e> ∈ EXTI(I(owl:oneOf))です。したがって、IはT(F)を満たします。
IがT(F)を満たす場合、IはT(SEQ i1 … in)を満たします。したがって、<I(foo),I+A(M(T(SEQ i1 … in)))> ∈ EXTI(I(owl:oneOf))であるような、上記のような、あるAが存在します。したがって、{SI(M(T(i1)), …, SI(M(T(in))} = CEXTI(I(foo)) = EC(foo)です。したがって、I'はFを満たします。
ここで唯一示す必要があるものは、fooのタイプ付けであり、それはクラスに対するものに似ています。
diはV'上の記述であるため、IはT(di)を満たし、I+AがT(di)を満たすようなT(di)の空白ノードをマッピングする任意のAに対し、CEXTI(I+A(M(T(di)))) = EC(di)です。
IがT(F)を満たす場合、1≤i≤nに対し、1≤i<j≤nごとに、Iが<I+Ai(M(T(di))),I+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith))を満たすような、あるAiが存在します。したがって、EC(di)∩EC(dj) = {}です(i≠jに対し)。したがって、I'はFを満たします。
I'がFを満たす場合、i≠jに対し、EC(di)∩EC(dj) = {}です。上記の任意のAiおよびjに対し、<I+Ai+Aj(M(T(di))),I+Ai+Aj(M(T(dj)))> ∈ EXTI(I(owl:disjointWith))です(i≠jに対し)。少なくとも1つのAiがiごとに存在し、T(dj)の空白ノードがすべて互いに素であるため、I+A1+…+AnはT(DisjointClasses(d1 … dn))を満たします。したがって、IはT(F)を満たします。
1≤i≤mに対するdiがV'上の記述であるため、IはT(di)を満たし、I+AがT(di)を満たすようなT(di)の空白ノードをマッピングする任意のAに対し、CEXTI(I+A(M(T(di)))) = EC(di)です。1≤i≤kに対するriに対しても同様です。
I'がFを満たす場合、p∈VOPであるため、IはI(p)∈IOOPを満たします。このとき、IはOWL DL解釈であるため、Iは<I(p),I(owl:Thing)>∈EXTI(I(rdfs:domain))、かつ、<I(p),I(owl:Thing)>∈EXTI(I(rdfs:range))を満たします。さらに、1≤i≤nに対し、ER(p)⊆ER(si)であり、よって、EXTI(I(p))=ER(p) ⊆ ER(si)=EXTI(I(si))、かつ、Iは<I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf))を満たします。次に、1≤i≤mに対し、ER(p)⊆EC(di)×Rであり、よって<z,w>∈ER(p)はz∈EC(di)を意味し、かつ、I+AがT(di)を満たすような任意のAに対し、<z,w>∈EXTI(p)はz∈CEXTI(I+A(M(T(di))))を意味し、したがって<I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain))です。1≤i≤kに対するriに対しても同様です。
I'がFを満たし、inverse(i)がFに存在する場合、ER(p)とER(i)は逆です。したがって、<v,u>∈ER(i)である場合に限り、<u,v>∈ER(p)であり、よって、<v,u>∈EXTI(i)、かつ、Iが<I(p),I(i)>∈EXTI(I(owl:inverseOf))を満たす場合に限り、<u,v>∈EXTI(p)です。I'がFを満たし、対称的がFに存在する場合、ER(p)は対称的です。したがって、<x,y>∈ ER(p)である場合、<y,x>∈ER(p)であり、よって、<x,y> ∈ EXTI(p)である場合、<y, x>∈EXTI(p)です。また、したがって、Iはp∈CEXTI(I(owl:Symmetric))を満たします。関数型、逆関数型、および推移的に対しても同様です。したがって、I'がFを満たす場合、IはT(F)を満たします。
IがT(F)を満たす場合、1≤i≤nに対し、<I(p),I(si)>∈EXTI(I(rdfs:subPropertyOf))であり、よって、ER(p)=EXTI(I(p)) ⊆ EXTI(I(si))=ER(si)です。さらに、1≤i≤mに対し、I+AがT(di)を満たすような、あるAに対し、<I(p),I+A(M(T(di)))>∈EXTI(I(rdfs:domain))であり、よって、<z,w>∈EXTI(p)はz∈CEXTI(I+A(M(T(di))))を意味します。したがって、<z,w>∈ER(p)はz∈EC(di)、かつ、ER(p)⊆EC(di)×Rを意味します。1≤i≤kに対するriに対しても同様です。
IがT(F)を満たし、inverse(i)がFに存在する場合、Iは<I(p),I(i)>∈EXTI(I(owl:inverseOf))を満たします。したがって、<v,u>∈EXTI(i)である場合に限り、<u,v>∈EXTI(p)であり、よって、<v,u>∈ER(i)である場合に限り、<u,v>∈ER(p)、かつ、ER(p)とER(i)は逆です。IがFを満たし、対称的がFに存在する場合、Iはp∈CEXTI(I(owl:Symmetric))を満たし、よって、<x,y> ∈ EXTI(p)である場合、<y, x>∈EXTI(p)です。したがって、<x,y>∈ ER(p)である場合、<y,x>∈ER(p)、かつ、ER(p)は対称的です。関数型、逆関数型、および推移的に対しても同様です。したがって、IがT(F)を満たす場合、I'はFを満たします。
pi∈VOP、かつ、IがT(V')を満たすため、I(pi)∈IOOPです。IがT(F)を満たす場合、<I(pi),I(pj)> ∈ EXTI(I(owl:equivalentProperty))です(1≤i<j≤nごとに)。したがって、EXTI(pi) = EXTI(pj)、かつ(1≤i<j≤nごとに)、ER(pi) = ER(pj)、(1≤i<j≤nごとに)、かつ、I'はFを満たします。
I'がFを満たす場合、ER(pi) = ER(pj)です(1≤i<j≤nごとに)。したがって、EXTI(pi) = EXTI(pj)(1≤i<j≤nごとに)。owl:equivalentPropertyのOWL DL定義から、<I(pi),I(pj)> ∈ EXTI(I(owl:equivalentProperty))です(1≤i<j≤nごとに)。したがって、IはT(F)を満たします。
IがT(F)を満たす場合、I+AがT(F)を満たすような、T(F)にそれぞれの空白ノードをマッピングする、あるAが存在します。T(F)の簡単な調査により、Aのマッピングに加え、Fの個体IDに対するマッピング(すべてIOTにおける)はI'がFを満たすことを示すということが分かります。
I'がFを満たす場合、Fの個体構成子ごとに、Fのタイプ関係および関係を真にするRの、ある要素がなければなりません。このとき、T(F)のトリプルは、3つのカテゴリーに分類されます。(1) owl:Thingとのタイプ関係(上記の要素がRに属するため、Iにおいて真である)。(2) 補助定理1から、OWL記述とのタイプ関係(I'において真であるため、Iにおいて真である)。(3) OWLプロパティー関係(Iにおいて真であるため、I'において真である)。したがって、IはT(F)を満たします。
補助定理3: V' = VO + VC + VD + VI + VOP + VDP + VAP + VXPを分離されたOWL語彙とします。V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VBとします。このとき、T(V')を満たすVのすべてのOWL DL解釈I = <RI,PI,EXTI,SI,LI,LVI>に対し、Oが閉じたインポートであるような語彙V'を持つ任意のOWL抽象オントロジーのコレクションおよび公理と事実Oに対し、IがOWL DLでT(O)を満たす場合に限り、I' がOを直接満たすような、直接解釈V'のI'が存在します。
証明:
CEXTIを、通常通り、Iからのものあると定義します。必要な直接解釈は、以下の場合、I' = < RI, EC, ER, L, S, LVI >です。
V'、V、I'、およびIは補助定理2の要件を満たし、よって、V'上の任意の命令Dに対し、I'がDを満たす場合に限り、IはT(D)を満たします。
Oは閉じたインポートであるため、OはT(O)でインポートされるすべてのオントロジーを含んでおり、よって、インポート命令のインポートする部分は同じように扱われます。抽象オントロジーを満たすことは、その命令を単に満たすだけであり、抽象オントロジーの翻訳を満たすことは、すべてのトリプルを満たすことであり、よって、I'がKを直接満たす場合に限り、IはOWL DLでT(K)を満たします。
補助定理4: V' = VO + VC + VD + VI + VOP + VDP + VAP + VXPを分離されたOWL語彙とします。V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VBとします。このとき、すべての直接解釈である、V'のI' = < U, EC, ER, L, S, LV >に対し、Oが閉じたインポートであるような、語彙V'を持つ任意のOWL抽象オントロジーのコレクションおよび公理と事実Oに対し、IがOWL DLでT(O)を満たす場合に限り、I'がOを直接満たすような、T(V')を満たすVのOWL DL解釈Iが存在します。
証明:
I = < RI, PI, EXTI, SI, L, LVI >を以下のように構築します。
このとき、OWL DLのクラス拡張に対する条件がクラス状のOWL抽象構文構成子に対する条件とマッチするため、IはOWL DL解釈です。
V'、V、I'、およびIは補助定理2の要件を満たし、よって、V'上の任意の命令Dに対し、I'がDを満たす場合に限り、IはT(D)を満たします。
Oは閉じたインポートであるため、OはT(O)でインポートされるすべてのオントロジーを含んでおり、よってインポート命令のインポートする部分は同じように扱われます。抽象オントロジーを満たすことは、その命令を単に満たすだけであり、抽象オントロジーの翻訳を満たすことは、すべてのトリプルを満たすことであり、よって、I'がKを直接満たす場合に限り、IはT(K)をOWL DLで満たします。
定理1: OおよびO'を、それらの和集合が分離された語彙V'を持ち、V'のすべてのURI参照がOで使用されるような、閉じたインポートである、抽象構文形式のOWL DLオントロジーのコレクションおよび公理と事実とします。このとき、T(O)がT(O')をOWL DL含意する場合に限り、OはO'を含意します。
このとき、V'のそれぞれのURI参照がOにおいて使用されるため、IはT(V')を満たします。
証明: OがO'を含意すると仮定します。IをT(O)を満たすOWL DL解釈とします。このとき、補助定理3から、任意の抽象OWLオントロジーあるいは公理または事実である、V'上のXに対し、I'がXを満たす場合に限り、IがT(X)を満たすような、ある直接解釈I'が存在します。したがって、I'はOのそれぞれのオントロジーを満たします。OがO'を含意するため、I'はO'を満たし、よって、IはT(O')を満たします。したがって、T(K)、T(V')は、T(Q)をOWL DL含意します。
T(O)がT(O')をOWL DL含意すると仮定します。I'を、Kを満たす直接解釈とします。このとき、補助定理4から、任意の抽象OWLオントロジーである、V'上のXに対し、I'がXを満たす場合に限り、IがT(X)を満たすような、あるOWL DL解釈Iが存在します。したがって、IはT(O)を満たします。T(O)がT(O')をOWL DL含意するため、IはT(O')を満たし、よって、I'はO'を満たします。したがって、OはO'を含意します。
この項には、OWL DLとOWL Fullの関係に関する証明のスケッチが含まれています。この証明は完全には出来上がっていません。証明を完成させるには非常な努力が必要かもしれませんし、関係のいくつかの詳細を変更しなければならないかもしれません。
KをRDFグラフとします。KのOWL解釈は、KのD解釈である、OWL解釈(5.2項から)です。
補助定理5: Vを分離された語彙とします。このとき、すべてのOWL解釈Iに対し、分離された語彙Vを持つ抽象構文における任意のOWLオントロジーであるKに対し、I'がT(K)のOWL DL解釈である場合に限り、IがT(K)のOWL解釈であるような、OWL DL解釈I'が存在します(5.3項と同様に)。
証明のスケッチ: すべてのOWL DL解釈はOWL解釈であるため、逆方向については自明です。
I = < RI, EXTI, SI, LI >をT(K)を満たすOWL解釈とします。I' = < RI', EXTI', SI', LI' >をT(K)を満たすOWL解釈とします。RI' = CEXTI(I(owl:Thing)) + CEXTI(I(owl:ObjectProperty)) + CEXTI(I(owl:ObjectProperty)) + CEXTI(I(owl:Class)) + CEXTI(I(rdf:List)) + RIとします(+が互いに素の和集合である場合)。コピーの様々な役割を分離するようにEXTI'を定義します。語彙を適切なコピーへマッピンするようにSI'を定義します。これは、Kが分離された語彙を持つため、機能します。よって、Iはその役割に従って分割され、EXTIには不適切な関係は存在しません。要するに、RI'の第1要素はOWL個体、RI'の第2要素はOWLデータ型プロパティー、RI'の第3要素はOWL個体値プロパティー、RI'の第4要素はOWLクラス、RI'の第5要素はRDFリスト、そしてRI'の第6要素はその他すべてです。
定理2: OおよびO'をそれらの和集合が分離された語彙(4.2項)を持っているような、閉じたインポートである、抽象構文形式のOWL DLオントロジーのコレクションおよび公理と事実とします。このとき、Oの翻訳がO'の翻訳をOWL DL含意する場合、Oの翻訳はO'の翻訳をOWL Full含意します。
証明: 上記の補助定理から、およびすべてのOWL Full解釈はOWL解釈であるため。
注: 方向が真でない場合のみ。