OWLウェブ・オントロジー言語
セマンティクスおよび抽象構文
付録A. 証明（参考情報）

付録A. 証明（参考情報）

この付録には、ドキュメントの5項に含まれる定理の証明が含まれています。

名称: この付録の全体にわたって、Dは、すべての組み込みOWLデータ型およびrdf:XMLLiteralに対するデータ型を含むデータ型マップ（3.1項）で、Tは、4.1項の抽象OWLオントロジーからRDFグラフへのマッピングです。そして、VBは組み込みOWL語彙です。さらに、語彙中のプレーンなリテラルについては言及しません。

注: この付録の全体にわたって、すべての解釈は、データ型マップDに関するのもです。したがって、すべての結果はDに関するものです。構築に関する分かりきったことの詳細の一部は省略しています。

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

この項では、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で形式化されます。

• オントロジー名として使用されるすべてのURI参照はVAから得られ、クラスIDはVCから得られ、データ型IDはVDから得られ、個体IDはVIから得られ、個体値プロパティーIDはVOPから得られ、データ値プロパティーIDはVDPから得られ、アノテーション・プロパティーIDはVAPから得られ、オントロジー・プロパティーIDはVXPから得られます。
• 個体IDとして使用されるすべてのURI参照は、Oのあるオントロジーにおいてタイプを与えられます。
• Oにおけるオントロジーおよび公理と事実は、クラス限定語彙（class-only vocabulary）のみをクラスIDとして使用し、データ型限定語彙（datatype-only vocabulary）のみをデータ型IDとして使用し、プロパティー限定語彙（property-only vocabulary）のみをdatavaluedProperty ID、individualvaluedProperty ID、annotationProperty ID、あるいはontologyProperty IDとして使用し、許されていない語彙（disallowed vocabulary）には少しも言及しません。

このとき、証明される定理は、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'の直接解釈とします。LV_I = LVであれば、I = <R_I,P_I,EXT_I,S_I,L_I,LV_I>をT(V')を満たすVのOWL DL解釈とします。CEXT_Iがその通常の意味を持っているものとし、かつ、いつものように、任意の構文構成子をその表示にマッピングするようにIをオーバーロード（overload）させます。もし、

• 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_I(owl:DeprecatedClass) > EXT_I(S_I(rdf:type))の場合に限り、< x, S(owl:DeprecatedClass) > ∈ ER(rdf:type)（x ∈ Rに対し）
• < x, S_I(owl:DeprecatedProperty) > EXT_I(S_I(rdf:type))の場合に限り、< x, S(owl:DeprecatedProperty) > ∈ ER(rdf:type)（x ∈ Rに対し）
• L(d)=L_I(d)（任意の型付きデータ・リテラルであるdに対し）
• S(v)=S_I(v)（v ∈ VI ∪ VC ∪ VD ∪ VOP ∪ VDP ∪ VAP ∪ VXP ∪ VOに対し）

である場合、任意の抽象OWL記述あるいはV'を超えるデータ値域である、dに対し、

1. IはT(d)を直接満たし、
2. I+AがT(d)をOWL DLで満たす、R_IへT(d)のすべての空白ノードをマッピングする任意のAに対し、
   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))です。

証明:

補助定理の証明は、構造帰納法（structural induction）によります。証明の全体にわたって、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))とします。

帰納法を機能させるためには、サブ構成子T(d)を持つ記述またはデータ値域である、任意の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はRDF互換でT(v)を満たします。M(T(v))がvであるため、CEXT_I(I(M(T(v))))=EC(v)です。最終的に、以上から、I(v)∈IDCです。

基本事例: d=oneOf(i₁…i_n)（i_jが個体IDsである場合）

1≤j≤nに対し、i_j∈VI、かつ、IがT(V)を満たすため、I(i_j)∈IOTです。このとき、数列に対する第2の内包原理（comprehension principle）は、IOT上のI(i₁),…,I(i_n)の数列である、l∈ILが存在することを要求します。IOT上のI(i₁),…,I(i_n)の数列である任意のlに対し、oneOfに対する内包原理は、<y,l> ∈ EXT_I(IS(owl:oneOf))であるような、y∈CEXT_I(I(rdfs:Class))が存在することを要求します。oneOfの第3の特性から、y∈IOCです。したがって、IはT(d)を満たします。T(d)を満たす任意のI+Aに対し、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であるため、このとき、数列に対する第2の内包原理は、LV_Iの上のI(v₁),…,I(v_n)の数列である、あるl∈ILが存在することを要求します。LV_I上のI(v₁),…,I(v_n)数列である任意のlに対し、oneOfに対する内包原理は、<y,l> ∈ EXT_I(IS(owl:oneOf))であるような、あるy∈CEXT_I(I(rdfs:Class))が存在することを要求します。oneOfの第2の特性から、y∈IOCです。したがって、IはT(d)を満たします。T(d)を満たす任意のI+Aに対し、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がindividualIDの条件で）

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')

帰納法の仮定（induction hypothesis）から、IはT(d')を満たします。d'が記述であるため、帰納法の仮定から、I+AがT(d')を満たし、I+A(M(T(d'))) = EC(d')、かつI+A(M(T(d')))∈IOCであるような、定義域要素にT(d')のすべての空白ノードをマッピングする、マッピング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を満たし、よって、I+A_iがT(d_i)を満たすような、定義域要素にT(d_i)のすべての空白ノードをマッピングする、マッピングA_iが存在します。T(di)の空白ノードがi≠jに対するT(d_j)の空白ノードと互いに素であるため、I+A₁+…+A_nであり、よってIはT(d_i)∪…∪T(d_n)を満たします。それぞれのd_iは記述であり、よって帰納法の仮定から、I+A₁+…+A_n(M(T(d_i)))∈IOCです。このとき、数列に対する第1の内包原理は、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))であるような、y∈IOCが存在することを要求し、よってIはT(d)を満たします。
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は、1≤i≤nに対し、restriction(p x_i)を満たし、よって、I+A_iがT(restriction(p x_i))を満たすような、定義域要素にT(restriction(p x_i))のすべての空白ノードをマッピングする、マッピングA_iが存在します。T(restriction(p x_i))の空白ノードがi≠jに対するT(restriction(p x_j))の空白ノードと互いに素であるため、I+A₁+…+A_nであり、よってIはT(restriction(p x₁ … x_n))を満たします。それぞれのrestriction(p x_i)は記述であり、よって帰納法の仮定から、M(T(restriction(p x_i)))∈IOCです。このとき、数列に対する第1の内包原理は、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))であるような、y∈IOCが存在することを要求し、よってIはT(d)を満たします。
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'が記述であるため、帰納法の仮定から、I+AがT(d')を満たすような定義域要素に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)を満たすことを示す形で、T(d')あるいはT(p)にないT(d)のトリプルをIが満たすことを要求します。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'上の抽象OWL個体構成子とします（Individual(…)形式の）。このとき、I+AがT(d)をOWL DLで満たす場合の、T(d)のすべての空白ノードをR_Iにマッピングする任意のAに対し、I+A(M(T(d))) ∈ EC(d)です。さらに、任意のr ∈ EC(d)に対し、I+A(M(T(d))) = rのような、T(d)のすべての空白ノードをR_IにマッピングするAが存在します。

証明:

シンプルな帰納論証（inductive argument）は、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と同様とします。Fをannotation(p x)形式のアノテーションを持つV'上のOWL命令とします。Fがクラスまたはプロパティー公理である場合、nをそのクラスあるいはプロパティーの名前とします。Fが個体の公理であれば、nをT(F)の主要ノードとします。このとき、T(F)のすべての空白ノードをR_Iにマッピングする任意の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の使用をちょうど要求するのと全く同じように動作します。したがって、残りの証明は、アノテーションを無視するでしょう。非推奨は、同様の方法で扱うことができ、これも残りの証明では無視されるでしょう。

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

d=intersectionOf(d₁ … d_n)とします。dはV'上の記述であるため、IはT(d)を満たし、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする任意のAに対し、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です。したがって、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする、あるAに対し、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)に属している場合、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です（1≤ j ≤mに対し）。よって、I(owl:unionOf)におけるセマンティック条件から、<I(foo),I+A(M(T(SEQ d₁₁ … d_1m)))> ∈ EXT_I(I(owl:unionOf))です。

したがって、IはT(F)を満たします（潜在的な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)とします。dがV'上の記述であるため、IはT(d)を満たし、I+AがT(d)を満たすような、T(d)のブ空白ノードをマッピングする任意のAに対し、CEXT_I(I+A(M(T(d)))) = EC(d)です。したがって、CEXT_I(I+A(M(T(d_i)))) = EC(d_i)です（1 ≤ i ≤ nに対し）。したがって、I+AがT(d)を満たすような、T(d)の空白ノードをマッピングする、あるAに対し、CEXT_I(I+A(M(T(d_i)))) = EC(d_i)、かつ、I+A(M(T(d_i))∈IOCです（1 ≤ i ≤ nに対し）。

I'がFを満たす場合、EC(foo) ⊆ EC(d_i)です（1 ≤ i ≤ nに対し）。以上から、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であり、したがって、<I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf))です（1 ≤ i ≤ nに対し）。したがって、IはT(F)を満たします。

IがT(F)を満たす場合、IはT(d_i)を満たします（1 ≤ i ≤ nに対し）。したがって、<I(foo),I+A(M(T(d_i)))> ∈ EXT_I(I(rdfs:subClassOf))（1 ≤ i ≤ nに対し）であるような、上記のような、あるAが存在します。したがって、EC(d) = CEXT_I(I+A(M(T(d_i)))) ⊇ CEXT_I(I(foo)) = EC(foo)です（1 ≤ i ≤ nに対し）。したがって、I' はFを満たします。

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

d=oneOf(i₁ … i_n)とします。dがV'上の記述であるため、ゆえに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))}です。さらに、S_I(M(T(i_j)) ∈ IOTです（1 ≤ j ≤ nに対し）。

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)

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)です。

IがT(F)を満たす場合、1≤i≤nに対し、1≤i<j≤nごとに、Iが<I+A_i(M(T(d_i))),I+A_j(M(T(d_j)))> ∈ EXT_I(I(owl:disjointWith))を満たすような、あるA_iが存在します。したがって、EC(d_i)∩EC(d_j) = {}です（i≠jに対し）。したがって、I'はFを満たします。

I'がFを満たす場合、i≠jに対し、EC(d_i)∩EC(d_j) = {}です。上記の任意のA_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≠jに対し）。少なくとも1つのA_iが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])

1≤i≤mに対する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)です。1≤i≤kに対する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))を満たします。さらに、1≤i≤nに対し、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))を満たします。次に、1≤i≤mに対し、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))です。1≤i≤kに対するr_iに対しても同様です。

I'がFを満たし、inverse(i)がFに存在する場合、ER(p)とER(i)は逆です。したがって、<v,u>∈ER(i)である場合に限り、<u,v>∈ER(p)であり、よって、<v,u>∈EXT_I(i)、かつ、Iが<I(p),I(i)>∈EXT_I(I(owl:inverseOf))を満たす場合に限り、<u,v>∈EXT_I(p)です。I'がFを満たし、対称的が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))を満たします。関数型、逆関数型、および推移的に対しても同様です。したがって、I'がFを満たす場合、IはT(F)を満たします。

IがT(F)を満たす場合、1≤i≤nに対し、<I(p),I(s_i)>∈EXT_I(I(rdfs:subPropertyOf))であり、よって、ER(p)=EXT_I(I(p)) ⊆ EXT_I(I(s_i))=ER(s_i)です。さらに、1≤i≤mに対し、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を意味します。1≤i≤kに対する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)である場合に限り、<u,v>∈ER(p)、かつ、ER(p)とER(i)は逆です。IがFを満たし、対称的が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)は対称的です。関数型、逆関数型、および推移的に対しても同様です。したがって、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)を満たす場合、<I(p_i),I(p_j)> ∈ EXT_I(I(owl:equivalentProperty))です（1≤i<j≤nごとに）。したがって、EXT_I(p_i) = EXT_I(p_j)、かつ（1≤i<j≤nごとに）、ER(p_i) = ER(p_j)、（1≤i<j≤nごとに）、かつ、I'はFを満たします。

I'がFを満たす場合、ER(p_i) = ER(p_j)です（1≤i<j≤nごとに）。したがって、EXT_I(p_i) = EXT_I(p_j)（1≤i<j≤nごとに）。owl:equivalentPropertyのOWL DL定義から、<I(p_i),I(p_j)> ∈ EXT_I(I(owl:equivalentProperty))です（1≤i<j≤nごとに）。したがって、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のマッピングに加え、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)を満たします。

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とします。このとき、T(V')を満たすVのすべてのOWL DL解釈I = <R_I,P_I,EXT_I,S_I,L_I,LV_I>に対し、Oが閉じたインポートであるような語彙V'を持つ任意のOWL抽象オントロジーのコレクションおよび公理と事実Oに対し、IがOWL DLでT(O)を満たす場合に限り、I' がOを直接満たすような、直接解釈V'のI'が存在します。

証明:

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はOWL DLでT(K)を満たします。

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 >に対し、Oが閉じたインポートであるような、語彙V'を持つ任意のOWL抽象オントロジーのコレクションおよび公理と事実Oに対し、IがOWL DLでT(O)を満たす場合に限り、I'がOを直接満たすような、T(V')を満たすVのOWL DL解釈Iが存在します。

証明:

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を許されてない語彙、マイナス、rdf:nilとします。
• R_IをU、IOC、IDC、IOP、IX、IL、IAD、およびIVの直和（disjoint union）とします。
• P_IをIOP ∪ IVとします。
• LV_I = LVとします。
  n∈VIに対し、S_I(n) = S(n)とします。
  n∈V-VIに対し、S_I(n) = nとします。
• c∈IOCに対し、定義されている場合は、EXT_I(r)=ER(r)、そうでない場合は、{}です。
  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がその末尾（tail）である場合に限り、<x,y> ∈ EXT_I(rdf:rest)
  EXT_I(S_I(rdfs:domain)) = { <x,y> : x∈IOP y∈IOC ∧ ∀ w, <w,z> ∈ EXT_I(x) implies w ∈ CEXT_I(y) }
  EXT_I(S_I(rdfs:range)) = { <x,y> : x∈OP y∈IOC ∧ ∀ z, <w,z> ∈ EXT_I(x) implies 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))は、IADの要素をILにおけるそれらのコピーに関連付けますが、別個の個体数列に対してのみです。
  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'を、それらの和集合が分離された語彙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'を含意します。

A.2 OWL DLとOWL Fullの対応

この項には、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 = < 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'の第1要素はOWL個体、R_I'の第2要素はOWLデータ型プロパティー、R_I'の第3要素はOWL個体値プロパティー、R_I'の第4要素はOWLクラス、R_I'の第5要素はRDFリスト、そしてR_I'の第6要素はその他すべてです。

定理2: OおよびO'をそれらの和集合が分離された語彙（4.2項）を持っているような、閉じたインポートである、抽象構文形式のOWL DLオントロジーのコレクションおよび公理と事実とします。このとき、Oの翻訳がO'の翻訳をOWL DL含意する場合、Oの翻訳はO'の翻訳をOWL Full含意します。

証明: 上記の補助定理から、およびすべてのOWL Full解釈はOWL解釈であるため。

注: 方向が真でない場合のみ。