附属書A(参考) 証明

この附属書は，規定の5.の定理の証明を記述する。

命名 この附属書を通して，Dは，すべての組込みOWLデータ型及びrdf:XMLLiteralのデータ型を含むデータ型対応付け(3.1)となる。Tは,抽象OWLオントロジから4.1のRDFグラフへの対応付けとなる。VBは，組込みOWL語い(彙)となる。同様に，語い(彙)中の普通リテラルには言及しない。

備考 この附属書を通して，すべての解釈はデータ型対応Dと関連する。したがって，すべての結果がDと関連する。構成の詳細は明らかにいくつか欠落している。

A.1 抽象OWLとOWL DLとの対応

A.1では，二つの意味論があるOWLオントロジに関して対応することを示す。二つの意味論とは，ここで直接モデル理論と呼ばれる3.の抽象OWLオントロジの直接モデル理論，及びここでOWL DLモデル理論と呼ばれる5.のOWL DL意味論とする。

定義 Dを上に示すとおりに仮定する場合，特別なOWL語い(彙) (4.2)は，ここではさらに形式化されてURI参照V'となり，V'の互いに素となる区画をもつ使用不能な語い(彙) (4.2)とは互いに素となる。これは，V' = VO + VC + VD + VI + VOP + VDP + VAP + VXPと書き込まれ，そこでは，組込みOWLクラスがVCに属し，URI参照，Dのすべてのデータ型名及びrdfs:Literalは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オントロジ及び公理並びに事実の集まりO(2.)は，ここでは，特別な語い(彙)の新しい概念V = VO + VC + VD + VI + VOP + VDP + VAP + VXPを用いて，さらに形式化される。次に例を示す。:

• オントロジ名として使用されるすべてのURI参照はVAから選択され，クラスIDはVCから，データ型IDはVDから，個体IDはVIから，個体値特性IDはVOPから，データ値特性IDはVDPから，注記特性IDはVAPから，オントロジ特性IDはVXPからそれぞれ選択される。
• 個体IDとして使用されるすべてのURI参照は，Oの何らかのオントロジの型を提供される。
• Oのオントロジ及び公理並びに事実は，クラスIDとして，クラス固有の語い(彙)だけを，データ型IDとして，データ型固有の語い(彙)だけを，データ値特性ID，個体値特性ID，注記特性ID，又はオントロジ特性IDとして，特性固有の語い(彙)だけをそれぞれ使用し，使用不能な語い(彙)には言及しない。

証明された定理は次となる。: O及びO'を閉鎖された取込みである抽象構文形式のOWL DLオントロジ及び公理並びに事実の集まりとする。その場合，それらの合併集合が特別な語い(彙)をもつものとし，その逆も成り立つ。その結果，T(O)がT(O')をOWL DLで論理的に帰結する場合に限り，OはO'を直接論理的に帰結し，その逆も成り立つ。

A.1.1 記述の対応

補助定理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'の直接解釈とする。I = <R_I,P_I,EXT_I,S_I,L_I,LV_I> を，T(V')を満たすVのOWL DL解釈とする。その場合，LV_I = LVが成立する。CEXT_Iに通常の意味をもたせ，構文上のあらゆる構成要素をその表示に対応付けるために，通常どおり，Iをオーバロードさせる。次 の場合を検討する。

• R = R_I
• EC(v)=CEXT_I(S_I(v)) の場合 v∈VC∪VD
• ER(v)=EXT_I(S_I(v)) の場合 v∈VOP∪VDP∪VAP∪VXP
• < x, S(owl:DeprecatedClass) > ∈ ER(rdf:type) iff < x, S_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type)) の場合 x ∈ R
• < x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type) iff < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type)) の場合 x ∈ R
• L(d)=L_I(d) の場合，dはすべての型付きデータリテラルとする。
• S(v)=S_I(v) の場合 v ∈ VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VO

さらに，dがあらゆる抽象OWL記述又はV'に関するデータ域である場合は次となる。

1. IはT(d)を直接満たし，
2. あらゆるAがT(d)のすべての空ノードをR_Iに対応付け，その場合に，I+AがT(d)をOWL DLで満たす場合は次となる。
   1. CEXT_I(I+A(M(T(d)))) = EC(d)，
   2. dが記述であれば，I+A(M(T(d)))∈CEXT_I(S_I(owl:Class)) となり，
   3. dがデータ域であれば，I+A(M(T(d)))∈CEXT_I(S_I(rdfs:Datatype)) となる。

証明

補助定理の証明は，構成的帰納法による。証明を通じて，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))，及び IL = CEXT_I(I(rdf:List))とする。

帰納作業を行うに当っては，あらゆるdについて，下位構成要素T(d)をもつ記述又はデータ域が，他の下位構成要素からの三つ組をもつ空ノードを共有しない各下位構成要素の三つ組を含むことを示す必要がある。Tの規則からこれを簡単に検証することができる。

p∈VOPであれば，Iは p∈IOOPを満たす。IはOWL DL解釈であるため，Iは <p,I(owl:Thing)>∈EXT_I(I(rdfs:domain)) 及び <p,I(owl:Thing)>∈EXT_I(I(rdfs:range))を満たす。したがって，IはT(p)を満たす。p∈VDPの場合も同様とする。

基本例: v ∈VC，これはowl:Thing及びowl:Nothingを取り込む。

v∈VC及びIはT(V)を満たすため，I(v)∈CEXT_I(I(owl:Class))となる。IはOWL DL解釈 CEXT_I(I(v))⊆IOTであるため，<I(v),I(owl:Thing)>∈EXT_I(I(rdfs:subClassOf))となる。したがって，IはT(v)をOWL DLで満たす。M(T(v))はvであるため，CEXT_I(I(M(T(v))))=EC(v)となる。よって，上からI(v)∈IOCとなる。

基本例: v ∈VD，これはrdfs:Literalを取り込む。

v∈VD及びIがT(V)を満たすため，I(v)∈CEXT_I(I(rdfs:Datatype))となる。IがOWL DL解釈 CEXT_I(I(v))⊆LV_Iであるため，<I(v),I(rdfs:Literal)>∈EXT_I(I(rdfs:subClassOf))となるため，Iは，T(v)をRDF互換性で満たす。M(T(v))はvとする。したがって，CEXT_I(I(M(T(v))))=EC(v)となる。よって，上から，I(v)∈IDCとなる。

基本例: d=oneOf(i₁…i_n)，この場合，i_jは個体IDとする。

i_j∈VIの場合，1jnであるため，IがT(V)を満たすため，I(i_j)∈IOTとなる。シーケンスの二つ目の包括原理は，IOTに関して I(i₁),…,I(i_n)のシーケンスである何らかのl∈ILの存在を必す(須)とする。IOTに関するすべてのlが I(i₁),…,I(i_n)のシーケンスである場合，oneOfの包括原理は，<y,l> ∈ EXT_I(I(owl:oneOf))など，何らかのy∈CEXT_I(I(rdfs:Class))の存在を必す(須)とする。oneOfの三つ目の特徴から，y∈IOCとなる。そのため，IはT(d)を満たす。すべてのI+AがT(d)を満たす場合，CEXT_I(I+A(M(T(d)))) = {I(i₁),…,I(i_n)} = EC(d)となる。よって，I+A(M(T(d)))∈IOCとなる。

基本例: d=oneOf(v₁…v_n)，この場合v_iはデータリテラルとする。

I(v_j)∈LV_Iであるため，シーケンスの二つ目の包括原理は，LV_Lについて，I(v₁),…,I(v_n)のシーケンスである何らかのl∈ILの存在を必す(須)とする。すべてのlがLV_Iに関して I(v₁),…,I(v_n)のシーケンスである場合，oneOfの包括原理は，<y,l> ∈ EXT_I(IS(owl:oneOf))など，何らかのy∈CEXT_I(I(rdfs:Class))の存在を必す(須)とする。oneOfの二つ目の特徴から，y∈IOCとなる。そのため，IはT(d)を満たす。すべてのI+AがT(d)を満たす場合，CEXT_I(I+A(M(T(d)))) = {I(i₁),…,I(i_n)} = EC(d)となる。よって，I+A(M(T(d)))∈IDCとなる。

基本例: d=restriction(p value(i))で，p∈VOP∪VDPとなり，iが個体IDである場合

p∈VOP∪VDPであるため，上の記述からIはT(p)を満たす。IはT(V')を満たすため，I(p)∈IOOP∪IODPとする。i∈VI及びIがT(V')を満たすため，I(i)∈IOTとなる。制限の包括原理から，IはT(d)を満たす。I+AがT(d)を満たすようなあらゆるAについて，CEXT_I(I+A(M(T(d)))) = { x∈IOT | <x,I(i)> ∈EXT_I(p) } = { x∈R | <x,S(i)> ∈ER(p) } = EC(d)となる。よって，I+A(M(T(d)))∈IOCとなる。

基本例: d=restriction(p value(i))でp∈VOP∪VDPとなり，iが型付けされたデータ値である場合

同様となる。

基本例: d=restriction(p minCardinality(n))で，p∈VOP∪VDPとなり，nが負ではない整数の場合

同様となる。

基本例: d=restriction(p maxCardinality(n))で，p∈VOP∪VDPとなり，nが負ではない整数の場合

同様となる。

基本例: d=restriction(p Cardinality(n))で，p∈VOP∪VDPとなり，nが負ではない整数の場合

同様となる。

帰納的な例: d=complementOf(d')

帰納仮定から，IはT(d')を満たす。d'が記述であるため，帰納仮定から，T(d')のすべての空ノードを，I+AがT(d')を満たし，I+A(M(T(d'))) = EC(d')及びI+A(M(T(d')))∈IOCとなるような領域要素に対応付ける対応付けAが存在する。complementOfの包括原理は，I+Aが <y,e>∈EXT_I(I(owl:complementOf))を満たすようなy∈IOCの存在を必す(須)とし，それによりIはT(d)を満たす。T(d)を満たすあらゆるI+Aについて，CEXT_I(I+A(M(T(d)))) = IOT-CEXT_I(I+A(M(T(d)))) = R-EC(d') = EC(d)となる。よって，I+A(M(T(d)))∈IOCとなる。

帰納的な例: d = unionOf(d₁ … d_n)

帰納仮定から，Iは，1⊆i⊆nである場合に，d_iを満たす。それによって，T(d_i)のすべての空ノードをI+A_iがT(d_i)を満たすような領域要素に対応付ける対応付けA_iが存在する。T(d_i)の空ノードは，i≠j，I+A₁+…＋A_nの場合のT(d_j)の空ノードとは互いに素であるため，Iは，T(d_i)∪…∪T(d_n)を満たす。各d_iは記述であるため，帰納仮定から，I+A₁+…+A_n(M(T(d_i)))∈IOCが成立する。シーケンスの最初の包括原理は，IOCに関して，I+A₁+…+A_n(M(T(d₁))),…, I+A₁+…+A_n(M(T(d_n)))のシーケンスとなる何らかのl∈ILの存在を必す(須)とする。unionOfの包括原理は，<y,l>∈EXT_I(I(owl:unionOf))となり，それによってIがT(d)を満たすような何らかのy∈IOCの存在を必す(須)とする。
T(d)を満たすあらゆるI+Aについて，I+AはT(d_i)を満たし，それによって，CEXT_I(I+A(d_i)) = EC(d_i))となる。そのため，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)が成立する。よって，I(M(T(d)))∈IOCとなる。

帰納的な例: d = intersectionOf(d₁ … d_n)の場合

同様となる。

帰納的な例: d = restriction(p x₁ x₂ … x_n)

p∈VOP∪VDPであるため，上の記述から，IはT(p)を満たす。帰納仮定から，Iは，1inの場合のrestriction(p x_i)を満たす。それによって，T(restriction(p x_i))のすべての空ノードを，I+A_iがT(restriction(p x_i))を満たすような領域要素に対応付ける対応付け，A_iが存在する。T(restriction(p x_i))の空ノードは，i≠j，I+A₁+…+A_nの場合の T(restriction(p x_j))の空ノードとは互いに素であるため，Iは，T(restriction(p x₁ … x_n))を満たす。各restriction(p x_i)は記述であるため，帰納仮定から，M(T(restriction(p x_i)))∈IOCとなる。シーケンスの最初の包括原理は，IOCに関して，I+A₁+…+A_n(M(T(restriction(p x_i)))),…, I+A₁+…+A_n(M(T(restriction(p x_i))))のシーケンスとなる何らかのl∈ILの存在を必す(須)とする。intersectionOfの包括原理は，<y,l>∈EXT_I(I(owl:intersectionOf))が成立し，それによりIがT(d)を満たすような何らかのy∈IOCの存在を必す(須)とする。
T(d)を満たすあらゆるI+Aについて，I+AはT(d_i)を満たす。それによって CEXT_I(I+A(d_i)) = EC(d_i))となる。そのため，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)が成立する。よって，I(M(T(d)))∈IOCとなる

帰納的な例: d = restriction(p allValuesFrom(d'))で，p∈VOP∪VDPとなり，d'が記述である場合

p∈VOP∪VDPであるため，上の記述から，IはT(p)を満たす。帰納仮定から，IはT(d')を満たす。d'は記述であるため，帰納仮定から，T(d')のすべての空ノードを，I+AがT(d')を満たすような領域要素に対応付けるあらゆる対応付けAについて，I+A(M(T(d'))) = EC(d')かつI+A(M(T(d')))∈IOCが成立する。p∈VOP∪VDPであり，かつIがT(V')を満たすため，I(p)∈IOOP∪IODPとなる。allValuesFrom制限の包括原理は，IがT(d)を満たすことを示す方法で，IがT(d')又はT(p)には存在しないT(d)の三つ組を満たすことを必す(須)とする。
T(d)を満たすあらゆるI+Aについて，CEXT_I(I+A(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)が成立する。よって，I+A(M(T(d)))∈IOCとなる。

帰納的な例: d = restriction(p someValuesFrom(d))で，p∈VOP∪VDPかつd'が記述である場合

同様となる。

帰納的な例: d = restriction(p allValuesFrom(d))で，p∈VOP∪VDPかつd'がデータ域である場合

同様となる。

帰納的な例: d = restriction(p someValuesFrom(d))で，p∈VOP∪VDPかつ d'がデータ域である場合

同様となる。

補助定理1.1 V', V, I'，及びIを補助定理1の場合と同様とする。dをV'に関するIndividual(…)形式の抽象OWL個体構成要素とする。あらゆるAがT(d)のすべての空ノードをR_Iに対応付ける場合，I+AがT(d)をOWL DLで満たすのであれば，I+A(M(T(d))) ∈EC(d)が成立する。同様に，あらゆるr ∈EC(d)について，T(d)のすべての空ノードをI+A(M(T(d))) = rとなるようなR_Iに対応付ける何らかのAが存在する。

証明

簡単な帰納引数は，I+A(M(T(d)))がEC(d)のすべての要件を満たさなければならないことを示す。別の帰納引数が下位構成要素の空ノードの非共有に依存する場合，各r ∈EC(d)について，I+A(M(T(d))) = rとなるような何らかのAが存在することを示す。

A.1.2 指示文の対応

補助定理1.9 V', V, I'，及びIを補助定理1の場合と同様にする。V'に関して，FをOWL指示文とし，annotation(p x)形式の注記をもつものとする。Fがクラス又は特性の公理である場合，nをクラス又は特性の名前とする。Fが個体の公理である場合，nをT(F)の主ノードとする。その場合，あらゆるAがT(F)のすべての空ノードをR_Iに対応付けるのであれば，I+Aは，I'が注記による結果としての条件を直接満たす場合に限り，注記による結果としての三つ組をOWL DLで満たし，その逆も成り立つ。

証明

URI参照の注記について，意味論条件及び翻訳の三つ組を検査することによって，補助定理を簡単に確立することができる。Individual(...)の注記の場合は，補助定理1.1の使用も必要となる。

補助定理2 V', V, I'，及びIを補助定理1の場合と同様にする。V'に関して，FをOWL指示文とする。その場合，I'がFを満たす場合に限り，IはT(F)を満たし，その逆も成り立つ。

証明

証明の主要部分は，指示文に関しては，構成的帰納法とする。注記は多くの指示文で現れ，全く同様に作用する。そのため，注記は補助定理1.9の使用だけを必す(須)とする。したがって，証明の残りの部分は，注記を無視することになる。非推奨を同じ方法で取扱うことができ，証明の残りの部分では同様に無視されることになる。

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

d=intersectionOf(d₁ … d_n)とする。V'に関して，dは記述であるため，IはT(d)を満たし，あらゆるAが，I+AがT(d)を満たすようなT(d)の空ノードを対応付ける場合は，CEXT_I(I+A(M(T(d)))) = EC(d)となる。したがって，dのあらゆる下位記述であるd'について，CEXT_I(I+A(M(T(d')))) = EC(d')及びI+A(M(T(d')))∈IOCが成立する。 何らかのAが，I+AがT(d)を満たすようなT(d)の空ノードを対応付ける場合，CEXT_I(I+A(M(T(d)))) = EC(d)及びI+A(M(T(d)))∈IOCが成立する。さらにdの下位記述である各d'については，CEXT_I(I+A(M(T(d')))) = EC(d')， 及びI+A(M(T(d')))∈IOCが成立する。

I'がFを満たす場合，EC(foo) = EC(d)となる。上の記述から，CEXT_I(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(I(foo)) かつI+A(M(T(d)))∈IOCとなるような何らかのAが存在する。IがT(V)を満たすため，I(foo)∈IOCとなり，したがって，<I(foo),I+A(M(T(d)))> ∈ EXT_I(I(owl:equivalentClass))となる。さらに，I(owl:intersectionOf)の意味論条件のため，<I(foo),I+A(M(T(SEQ d₁ … d_n)))> ∈EXT_I(I(owl:intersectionOf))となる。

dがintersectionOf(d₁)形式に属する場合，CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) かつ I+A(M(T(d₁)))∈IOCとなる。そのため，I(owl:equivalentClass)の意味論条件から，<I(foo),I+A(M(T(d₁)))> ∈ EXT_I(I(owl:equivalentClass))となる。d₁がcomplementOf(d'₁)形式に属する場合，IOT - CEXT_I(I+A(M(T(d'₁)))) = CEXT_I(I+A(M(T(d₁)))) = EC(d₁) = EC(d) = EC(foo) かつ I+A(M(T(d'₁)))∈IOCとなる。そのため，I(owl:complementOf)の意味論条件から， <I(foo),I+A(M(T(d'₁)))> ∈ EXT_I(I(owl:complementOf))となる。d₁が unionOf(d₁₁ … d_1m)形式に属する場合，1jmであれば，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) かつ I+A(M(T(d_1j)))∈IOCとなる。そのため，I(owl:unionOf)の意味論条件から，<I(foo),I+A(M(T(SEQ d₁₁ … d_1m)))> ∈ EXT_I(I(owl:unionOf))となる。

その結果，潜在的な各T(F)について，IはT(F)を満たす。

IがT(F)を満たす場合，Iは，T(intersectionOf(d₁ … d_n))を満たす。したがって，上の記述のとおり，<I(foo),I+A(M(T(d)))> ∈ EXT_I(I(owl:equivalentClass))となるような何らかのAが存在する。したがって，EC(d) = CEXT_I(I+A(M(T(d)))) = CEXT_I(I(foo)) = EC(foo)となる。その結果，I'はFを満たす。

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

d=intersectionOf(d₁ … d_n)とする。V'に関して，dが記述であるため，IはT(d)を満たし，I+AがT(d)を満たすようなT(d)の空ノードを対応付けするあらゆるAについて，CEXT_I(I+A(M(T(d)))) = EC(d)が成立する。したがって，1 i nであれば，CEXT_I(I+A(M(T(d_i)))) = EC(d_i)となる。 そのため，I+AがT(d)を満たすようなT(d)の空ノードを対応付ける何らかのAについて，1 i nであれば，CEXT_I(I+A(M(T(d_i)))) = EC(d_i)， かつ I+A(M(T(d_i))∈IOCが成立する。

I'がFを満たす場合，1 i nであれば，EC(foo) ⊆EC(d_i)が成立する。上の記述から，CEXT_I(I+A(M(T(d_i)))) = EC(d_i) ⊇ EC(foo) = CEXT_I(I(foo)) かつI+A(M(T(d_i))∈IOCとなるような何らかのAが存在する。IがT(V)を満たすため，I(foo)∈IOCとなり，1 i nであれば，<I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf))が成立する。その結果，IはT(F)を満たす。

IがT(F)を満たす場合，1 i nであれば，Iは T(d_i)を満たす。したがって，1 i nであれば，上の記述のとおり，<I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf))となるような何らかのAが存在する。その結果，1 i nであれば，EC(d) = CEXT_I(I+A(M(T(d_i)))) ⊇ CEXT_I(I(foo)) = EC(foo)が成立する。よって，I'はFを満たす。

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

d=oneOf(i₁ … i_n)とする。V'に関して，dは記述であるため，IはT(d)を満たし，I+AがT(d)を満たすようなT(d)の空ノードを対応付ける何らかのAについて，EC(d) = CEXT_I(I+A(M(T(d)))) = {S_I(M(T(i₁)), … S_I(M(T(i_n))}となる。同様に，1 j nであれば，S_I(M(T(i_j)) ∈IOTが成立する。

I'がFを満たす場合，EC(foo) = EC(d)となる。上の記述から，CEXT_I(I+A(M(T(d)))) = EC(d) = EC(foo) = CEXT_I(I(foo)) かつ I+A(M(T(d))∈IOCとなるような何らかのAが存在する。 eをI+A(M(T(SEQ i₁ … i_n)))とする。それによって，I(owl:oneOf)の意味論条件から，<I(foo),e> ∈ EXT_I(I(owl:oneOf))となる。よって，IはT(F)を満たす。

IがT(F)を満たす場合，Iは，T(SEQ i₁ … i_n)を満たす。したがって，上の記述のとおり， <I(foo),I+A(M(T(SEQ i₁ … i_n)))> ∈ EXT_I(I(owl:oneOf))となるような何らかのAが存在する。その結果， {S_I(M(T(i₁)), …, S_I(M(T(i_n))} = CEXT_I(I(foo)) = EC(foo)が成立する。よって，I'はFを満たす。

例: F = Datatype(foo)

ここで示す必要があるのは，fooの型付けだけであり，これはクラスの型付けと同様とする。

例: F= DisjointClasses(d₁ … d_n)

V'に関して，d_iが記述であるため，IはT(d_i)を満たし，I+AがT(d_i)を満たすようなT(d_i)の空ノードを対応付けるあらゆるAについて，CEXT_I(I+A(M(T(d_i)))) = EC(d_i)が成立する。

IがT(F)を満たす場合，1inであれば，それぞれ1i<jnの条件下で，Iが <I+A_i(M(T(d_i))),I+A_j(M(T(d_j)))> ∈EXT_I(I(owl:disjointWith))を満たすような何らかのA_iが存在する。したがって，i≠jであれば，EC(d_i)∩EC(d_j) = {}となる。よって，I'はFを満たす。

I'がFを満たす場合，i≠jであれば，EC(d_i)∩EC(d_j) = {}となる。あらゆるA_i及びA_jについて，上の記述のとおり，i≠jであれば，<I+A_i+A_j(M(T(d_i))),I+A_i+A_j(M(T(d_j)))> ∈EXT_I(I(owl:disjointWith))が成立する。各iについて，少なくとも一つのA_iが存在し，T(d_j)の空ノードはすべて互いに素であるため，I+A₁+…+A_nは T(DisjointClasses(d₁ … d_n))を満たす。よって，IはT(F)を満たす。

例: F = EquivalentClasses(d₁ … d_n)

同様となる。

例: F = SubClassOf(d₁ d2)

若干類似する。

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

1imの場合にd_iはV'に関して記述となるため，IはT(d_i)を満たし，I+AがT(d_i)を満たすようなT(d_i)の空ノードを対応付けるあらゆるAについて，CEXT_I(I+A(M(T(d_i)))) = EC(d_i)が成立する。1ikの場合のr_iについても同様となる。

I'がFを満たす場合，p∈VOPであるため，IはI(p)∈IOOPを満たす。IはOWL DL解釈であるため，Iは <I(p),I(owl:Thing)>∈EXT_I(I(rdfs:domain)) 及び<I(p),I(owl:Thing)>∈EXT_I(I(rdfs:range))を満たす。同様に，1inの場合，ER(p)⊆ER(s_i)となるため，EXT_I(I(p))=ER(p)⊆ ER(s_i)=EXT_I(I(s_i))が成立し，Iは <I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf))を満たす。次に，1imの場合，ER(p)⊆EC(d_i)×Rとなるため，<z,w>∈ER(p)はz∈EC(d_i)を論理的に帰結し，I+AがT(d_i)を満たすようなあらゆるAについて，<z,w>∈EXT_I(p)は z∈CEXT_I(I+A(M(T(d_i))))を論理的に帰結する。したがって，<I(p),I+A(M(T(d_i)))>∈EXT_I(I(rdfs:domain))が成立する。1ikの場合のr_iについても同様となる。

I'がFを満たし，inverse(i)がFに属する場合，ER(p)及びER(i)は逆となる。したがって，<v,u>∈ER(i)である限り，<u,v>∈ER(p)となり，その逆も成り立つ。<v,u>∈EXT_I(i)である限り，<u,v>∈EXT_I(p)が成立し，その逆も成り立つため，Iは <I(p),I(i)>∈EXT_I(I(owl:inverseOf))を満たす。I'がFを満たし，SymmetricがFに属する場合，ER(p)は対称的となる。したがって，<x,y>∈ER(p)である場合，<y,x>∈ER(p)となり，それによって，<x,y> ∈EXT_I(p)の場合，<y, x>∈EXT_I(p)が成立する。よって，Iは p∈CEXT_I(I(owl:Symmetric))を満たす。Functional，InverseFunctional，及びTransitiveについても同様となる。よって，I'がFを満たす場合，IはT(F)を満たす。

IがT(F)を満たす場合，inであれば，<I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf))となり，それによって，ER(p)=EXT_I(I(p)) ⊆ EXT_I(I(s_i))=ER(s_i)となる。同様に，1imの場合，I+AがT(d_i)を満たすような何らかのAについて，<I(p),I+A(M(T(d_i)))>∈EXT_I(I(rdfs:domain))が成立し，それによって，<z,w>∈EXT_I(p)はz∈CEXT_I(I+A(M(T(d_i))))を論理的に帰結する。したがって，<z,w>∈ER(p)はz∈EC(d_i)及び ER(p)⊆EC(d_i)×Rを論理的に帰結する。1ikの場合のr_iについても同様となる。

IがT(F)を満たし，inverse(i)がFに属する場合，Iは <I(p),I(i)>∈EXT_I(I(owl:inverseOf))を満たす。したがって，<v,u>∈EXT_I(i)である場合に限り，<u,v>∈EXT_I(p)となり，その逆も成り立つため，<v,u>∈ER(i)であり，ER(p)及びER(i)が逆となる場合に限り，<u,v>∈ER(p)が成立し，その逆も成り立つ。IがFを満たし，SymmetricがFに属する場合，Iはp∈CEXT_I(I(owl:Symmetric))を満たす。それによって，<x,y> ∈EXT_I(p)であれば，<y, x>∈EXT_I(p)となる。したがって，<x,y>∈ER(p)であれば，<y,x>∈ER(p)が成立し，ER(p)は対称的となる。Functional, InverseFunctional，及びTransitiveについても同様となる。よって，IがT(F)を満たす場合，I'はFを満たす。

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

同様となるが，より簡単である。

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

同様となるが，より一層簡単である。

同様となるが，より一層簡単である。F = OntologyProperty(p domain(d₁) … domain(d_m))

例:

例: F = EquivalentProperties(p₁ … p_n), ただし，p_i∈VOPの場合

p_i∈VOPであり，IがT(V')を満たすため，I(p_i)∈IOOPが成立する。IがT(F)を満たす場合，それぞれ1i<jnであれば，<I(p_i),I(p_j)> ∈EXT_I(I(owl:equivalentProperty))となる。そのため，それぞれ1i<jnであれば，EXT_I(p_i) = EXT_I(p_j)となり，それぞれ1i<jnであれば，ER(p_i) = ER(p_j)となり，I'はFを満たす。

I'がFを満たす場合，それぞれ1i<jnであれば，ER(p_i) = ER(p_j)が成立する。そのため，それぞれ1i<jnであれば，EXT_I(p_i) = EXT_I(p_j)となる。owl:equivalentPropertyのOWL DL定義によって，それぞれ1i<jnであれば，<I(p_i),I(p_j)> ∈EXT_I(I(owl:equivalentProperty))となる。よって，IはT(F)を満たす。

例: F = SubPropertyOf(p₁ p₂)

若干類似するが，より簡単である。

例: F = SameIndividual(i₁ … i_n)

SamePropertyAsに類似する。

例: F = DifferentIndividuals(i₁ … i_n)

SamePropertyAsに類似する。

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

IがT(F)を満たす場合，I+AがT(F)を満たすようなT(F)の空ノードを各々対応付ける何らかのAが存在する。T(F)を簡単に検査することによって，Aの対応付け，さらに，そのすべてがIOTに属するFの個体IDに対する対応付けが，I'がFを満たすことを示していることがわかる。

I'がFを満たす場合，Fの各個体構成要素について，型関係及び関係をFで真にする何らかのRの要素が存在しなければならない。T(F)の三つ組は次の三種類に分かれる。1/ 上の要素がRに属するため，Iで真となる owl:Thingとの型関係。2/ I'で真となるため，補助定理1より，Iで真となるOWL記述との型関係。3/ Iで真となるため，I'で真となるOWL特性関係。よって，IはT(F)を満たす。

A.1.3 RDF意味論から直接的意味論への対応付け

補助定理3 V' = VO + VC + VD + VI + VOP + VDP + VAP + VXPを特別なOWL語い(彙)とする。V = VO ∪ VC ∪ VD ∪ VI ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VBとする。すべてのOWL DL解釈について，T(V')を満たすVに関して，I = <R_I,P_I,EXT_I,S_I,L_I,LV_I> となる場合，V'の直接解釈I'が存在する。この場合，OWL抽象オントロジ及び公理並びに事実Oのあらゆる集まりが，Oが閉鎖された取込みとなるような語い(彙)V'をもつ場合，IがT(O)をOWL DLで満たす限り，I'はOを直接満たし，その逆も成り立つ。

証明

CEXT_Iを，通常のとおり，Iから定義されるものとする。必す(須)とされる直接解釈は，次の場合，I' = < R_I, EC, ER, L, S, LV_I >となる。

1. EC(v) = CEXT_I(S_I(v))， この場合，v∈VC∪VDとなる。
2. ER(v) = EXT_I(S_I(v))， この場合，v∈VOP∪VDP∪VAP∪VXP となる。
3. < x, S_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type))である場合に限り，< x, S(owl:DeprecatedClass) > ∈ER(rdf:type)となり，その逆も成り立つ。この場合，x ∈Rとなる。
4. < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type))である場合に限り，< x,S(owl:DeprecatedProperty)> ∈ER(rdf:type)となり，その逆も成り立つ。この場合，x ∈Rとなる。
5. L(d) = L_I(d)， この場合，dは型付きリテラルとなる。
6. S(v) = S_I(v)， この場合，n∈VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VOとなる。

V', V, I'，及びIは，補助定理 2の要件を満たす。そのため，V'に関するあらゆる指示文Dについて，I'がDを満たす場合に限り，IはT(D)を満たし，その逆も成り立つ。

Oは閉鎖された取込みであるため，Oは，T(O)で取り込まれるすべてのオントロジを取り込み，取込み指示文の取込み部分を同様に扱うことになる。抽象オントロジを満たすことは，単にその指示文を満たしているにすぎず，抽象オントロジの翻訳を満たすことは，単にすべての三つ組を満たしているにすぎない。そのため，I'がKを直接満たす場合に限り，IはT(K)をOWL DLで満たし，その逆も成り立つ。

A.1.4 直接的意味論からRDF意味論への対応付け

補助定理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 >について，T(V')を満たすVのOWL DL解釈が存在する。この場合，Oが閉鎖された取込みとなるような語彙V'をもつOWL抽象オントロジ及び公理並びに事実のあらゆる集まりについて，IがT(O)をOWL DLで満たす場合に限り，I'がOを直接満たし，その逆も成り立つ。

証明

I = < R_I, P_I, EXT_I, S_I, L, LV_I >を次のとおり構成する。:

• IOCをV'に関するすべてのOWL記述とし，クラス固有の語い(彙)を追加する。
  IDCをV'に関するすべてのOWLデータ域とする。
  IOP = VOP ∪ VDP ∪ VAP ∪ VXPとし，特性固有の語い(彙)を追加する。
  IX = VOとする。
  ILをrdf:nilとし，U，IOC，及びLVに関する限定シーケンスを追加する。
  IADをrdf:nilとし，Uに関する限定シーケンスを追加する。
  IVを使用不能な語い(彙)とし，rdf:nilを除く。
• R_Iを互いに素となるU, IOC, IDC, IOP, IX, IL, IAD，及びIVの合併集合とする。
• P_IをIOP ∪ IVとする。
• LV_I = LVとする。
  S_I(n) = S(n)とし，この場合，n∈VIとする。
  S_I(n) = nとし，この場合，n∈V-VIとする。
• 定義される場合，c∈IOCであれば， CEXT_I(c)=EC(c)とし，それ以外の場合は{}とする。
  d∈IDCの場合，CEXT_I(d)=EC(d)となる。
  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))はRDF XMLリテラル値とする。
  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))はRDFコンテナメンバ関係特性とする。
  
• 定義される場合，r∈IOPであれば，EXT_I(r)=ER(r)となる。それ以外の場合，{}となる。
  
• EXT_I(S_I(rdf:type))は，CEXT_Iによって決定される。
  EXT_I(S_I(rdf:Property)) = EXT_I(S_I(rdf:List)) = EXT_I(S_I(rdf:XMLLiteral)) = {}
  x∈IL，かつ，yがその最初の要素である場合に限り，<x,y> ∈ EXT_I(rdf:first) となる。
  x∈IL，かつ，yがその末尾である場合に限り，<x,y> ∈EXT_I(rdf:rest)となる。
  EXT_I(S_I(rdfs:domain)) = { <x,y> : x∈IOP y∈IOC ∧ ∀ w, <w,z> ∈EXT_I(x)は，w ∈CEXT_I(y)を論理的に帰結する}
  EXT_I(S_I(rdfs:range)) = { <x,y> : x∈OP y∈IOC ∧ ∀ z, <w,z> ∈EXT_I(x)は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))はコンテナメンバ関係特性の拡張の合併集合とする。
  EXT_I(S_I(rdfs:Container)) = EXT_I(S_I(rdfs:ContainerMembershipProperty)) = {}
  
• owl:allValuesFrom, owl:cardinality, owl:hasValue, owl:maxCardinality, owl:minCardinality, owl:onProperty，及び owl:someValuesFromの拡張は，必要に応じて，それらの各部までIOC及びIDCの要素にリンクする。それらのクラス拡張はすべて空となる。
• owl:complementOf, owl:intersectionOf, owl:oneOf， 及びowl:unionOfの拡張は，必要に応じて，それらの意味論条件を正しく成立させる。それらのクラス拡張はすべて空となる。これらの拡張の修正は，その過程において何のループも帰納的に推論しないため，これは，ここでは，簡単に実行できる。
• 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)) は，その拡張が部分関数となるVOP∪VDP のそれらの要素とする。
  CEXT_I(S_I(owl:InverseFunctionalProperty))は，その拡張が逆部分関数となるVOPのそれらの要素とする。
  CEXT_I(S_I(owl:ObjectProperty)) = VOP
  CEXT_I(S_I(owl:Ontology)) = VO
  CEXT_I(S_I(owl:Restriction))は，OWL制限であるIOCのそれらの要素とする。
  CEXT_I(S_I(owl:SymmetricProperty))は，その拡張が対称となるVOPのそれらの要素とする。
  CEXT_I(S_I(owl:TransitiveProperty))は，その拡張が推移的となるVOPのそれらの要素とする。
  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))は，owl:distinctMembers特性をもつIADのそれらの要素から構成される。
  EXT_I(S_I(owl:differentFrom))は，Uに関しては，非同等関係とする。
  EXT_I(S_I(owl:disjointWith)) は，互いに素なクラス拡張をもつIOCのメンバを関連付ける。
  EXT_I(S_I(owl:distinctMembers))は，ILで，IADの要素をそれらのコピーに関連付けるが，識別可能な個体のシーケンスの場合に限られる。
  EXT_I(S_I(owl:equivalentClass))は，同じクラス拡張をもつIOCのメンバを関連付ける。
  EXT_I(S_I(owl:equivalentProperty))は，同じ拡張をもつIOP∪IDPのメンバを関連付ける。
  EXT_I(S_I(owl:inverseOf))は，その拡張が互いの逆となるIOPのメンバを関連付ける。
  EXT_I(S_I(owl:sameAs))は，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)) = {}

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で満たし，その逆も成り立つ。

A.1.5 対応定理

定理1 O及びO'を，閉鎖された取込みである抽象構文形式におけるOWL DLオントロジ及び公理並びに事実の集まりとし，それらの合併集合が特別な語い(彙)V'をもち，V'のすべてのURI参照がOで使用されるものとする。その場合，Oは，T(O)がT(O')をOWL DLで論理的に帰結する場合に限り，OはO'を論理的に帰結し，その逆も成り立つ。

その結果，V'の各URI参照がOで使用されるため，IはT(V')を満たす。

証明 OがO'を論理的に帰結すると想定する。IをT(O)を満たすOWL DL 解釈とする。その場合，補助定理3から，何らかの直接解釈I'が存在する。このI'は，V'に関するあらゆる抽象OWLオントロジ又は公理若しくは事実について，I'がXを満たす場合に限り，IがT(X)を満たすという性質をもち，その逆も成り立つ。したがって，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 DL解釈 Iが存在する。このIは，V'に関するあらゆる抽象OWLオントロジXについて，I'がXを満たす場合に限り，IはT(X)を満たす性質をもち，その逆も成り立つ。したがって，IはT(O)を満たす。T(O)がT(O')をOWL DLで論理的に帰結するため，IはT(O')を満たす。そのため，I'はO'を満たす。よって，OはO'を論理的に帰結する。

A.2 OWL DLとOWL Fullとの対応

A.2では，OWL DLとOWL Fullとの関係に関する証明概要を解説する。この証明は，十分に解明されたものではない。完全な証明を得るためには，大きな努力が必要とされ，その関係の詳細を幾つか変更する必要があるかもしれない。

KをRDFグラフとする。KのOWL解釈は，KのD解釈であるOWL解釈となる。5.2を参照されたい。

補助定理5 Vを特別な語い(彙)とする。その場合，すべてのOWL解釈Iについて，5.3の場合と同様に，OWL DL解釈I'が存在する。これは，Kについて，特別な語い(彙)Vをもつ抽象構文の中のあらゆるOWLオントロジIが，I'がT(K)のOWL DL解釈である場合に限り，T(K)のOWL解釈となる性質をもち，その逆も成り立つ。

証明概要: すべてのOWL DL解釈がOWL解釈となるため，逆指示文は明らかである。

I = < R_I, EXT_I, S_I, L_I > をT(K)を満たすOWL解釈とする。I' = < R_I', EXT_I', S_I', L_I' > をT(K)を満たすOWL解釈とする。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とする。この場合，+は互いに素な合併集合とする。コピーの様々な役割を区別するために，EXT_I'を定義する。語い(彙)を適切なコピーに対応付けるため，S_I'を定義する。Kが特別な語い(彙)をもつため，これは動作する。そのため，役割に従って，Iを分けることができ，EXT_Iに，不適切な関係は存在しない。本質的に，R_I'の最初の構成要素は，OWL個体であり，R_I'の2番目の構成要素は，OWLデータ型特性，R_I'の三番目の構成要素はOWL個体値特性，R_I'の四番目の構成要素はOWLクラス，R_I'の五番目の構成要素はRDFリスト，R_I'の六番目の構成要素はその他すべてのものとする。

補助定理2 O及びO'を，閉鎖された取込みである抽象構文の形式におけるOWL DLオントロジ及び公理並びに事実の集まりとする。この場合，それらの合併集合は，特別な語い(彙) (4.2)をもつものとする。それによって，Oの翻訳がO'の翻訳をOWL DLで論理的に帰結する場合，Oの翻訳は，O'の翻訳をOWL Fullで論理的に帰結する。

証明 上の補助定理，及びすべてのOWL Full解釈がOWL解釈であることを根拠とする。

備考 命令が真でない場合に限る。