OWLウェブ・オントロジー言語
セマンティクスおよび抽象構文
3項. 直接モデル理論セマンティクス

編集者:: Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies
Ian Horrocks, Department of Computer Science, University of Manchester

このドキュメントに対する正誤表を参照してください。いくつかの規範的な修正が含まれているかもしれません。

翻訳版も参照してください。

3. 直接モデル理論セマンティクス（規範）

このOWLのモデル理論セマンティクスは、OWL DL抽象構文（OWL Lite抽象構文を含む）のオントロジーから標準モデル理論へ直接的に展開します。これは、RDFSセマンティクスの語彙拡張である、5項のセマンティクスより単純です。

3.1. 語彙と解釈

ここでは、セマンティクスは、語彙の概念で始まります。OWLオントロジーについて考える場合、語彙は、オントロジーによってインポートされるオントロジーのみならず、すべてのURI参照およびリテラルをそのオントロジーに含んでいなければなりませんが、他のURI参照およびリテラルを含むこともできます。

この項では、V_OPは、組み込みOWLオントロジープロパティーに対するURI参照です。

定義: OWL語彙Vは、1組のリテラルV_Lおよび7組のURI参照、V_C、V_D、V_I、V_DP、V_IP、V_AP、およびV_Oから成ります。任意の語彙では、V_CとV_Dは互いに素で、V_DP、V_IP、V_AP、およびV_OPは、対で互いに素です。V_D（語彙のクラス名）は、owl:Thingおよびowl:Nothingを含んでいます。V_D（語彙のデータ型名）は、組み込みOWLデータ型およびrdfs:Literalに対するURI参照を含んでいます。V_AP（語彙のアノテーション・プロパティー名）は、owl:versionInfo、rdfs:label、rdfs:comment、rdfs:seeAlso、およびrdfs:isDefinedByを含んでいます。V_IP（語彙の個体値プロパティー名）、V_DP（語彙のデータ値プロパティー名）、およびV_I（語彙の個体名）、V_O（語彙のオントロジー名）には、既定のメンバーはありません。

定義: RDFと同様に、データ型dは、字句スペースL(d)（1組のUnicode文字列）、値スペースV(d)、および字句スペースから値スペースへのトータル・マッピングL2V(d)を特徴としています。

定義: データ型マップDは、xsd:stringおよびxsd:integerを適切なXMLスキーマ・データ型にマッピングする、URI参照からデータ型への部分的なマッピングです。

データ型マップは、他の組み込みOWLデータ型に対するデータ型を含むことができます。他のデータ型も含むことができますが、OWL構文には、これらのデータ型が何であるかを伝える方法が備わっていません。

定義: Dをデータ型マップとします。以下の場合、語彙V_L、V_C、V_D、V_I、V_DP、V_IP、V_AP、V_Oを持つDに関する抽象OWL解釈は、1組の形式I = <R, EC, ER, L, S, LV>です（Pが、べき集合（power set）演算子である場合）。

R（Iの資源）が空でない集合
LV（Iのリテラルの値）が、Unicode文字列の集合、対のUnicode文字列と言語タグの集合、およびDにおける各データ型に対する値スペース、を含んでいるRのサブセット
EC : V_C → P(O)
EC : V_D → P(LV)
ER : V_DP → P(O×LV)
ER : V_IP → P(O×O)
ER : V_AP ∪ { rdf:type } → P(R×R)
ER : V_OP → P(R×R)
L : TL → LV（TLがV_Lにおいて型付きリテラルの集合である場合）
S : V_I ∪ V_C ∪ V_D ∪ V_DP ∪ V_IP ∪ V_AP ∪ V_O ∪ { owl:Ontology, owl:DeprecatedClass, owl:DeprecatedProperty } → R
S(V_I) ⊆ O
EC(owl:Thing) = O ⊆ R（Oが空ではなく、LVとは互いに素である場合）

EC(owl:Nothing) = { }

EC(rdfs:Literal) = LV

If D(d') = d then EC(d') = V(d)

If D(d') = d then L("v"^^d') ∈ V(d)

If D(d') = d and v ∈ L(d) then L("v"^^d') = L2V(d)(v)

If D(d') = d and v ∉ L(d) then L("v"^^d') ∈ R - LV

ECは、OWLクラスおよびデータ型として使用されるURI参照に意味を与えます。ERは、OWLプロパティーとして使用されるURI参照に意味を与えます。（プロパティーrdf:typeは、非推奨に意味を与えるためにアノテーション・プロパティーに加えられます。下記を参照してください。）Lは、型付きリテラルに意味を与えます。Sは、OWL個体を示すために使用されるURI参照に意味を与え、アノテーションに意味を与えるのを助けます。不正形式のリテラル（つまり、1.5^^xsd:integerのように、その字句形式がデータ型では無効であるもの）に置かれた要件をすべて満たすことができる解釈がないことに注意してください。

Sは、リテラルを自身に（本質的に）マッピングすることにより、V_Lにおいてプレーンなリテラルに拡張されます、つまり、S("l") = l（言語タグのないプレーンなリテラルIに対して）、およびS("l"@t) = <l,t>（言語タグのないプレーンなリテラルIに対して）。Sは、Lの使用により型付きリテラル（S(l) = L(l)）に拡張されます（型付きリテラルIに対して）。

3.2. 組み込み構成子の解釈

ECは、EC拡張テーブルと同様に、記述、データ値域、個体、値、およびアノテーションの構文構成子に拡張されます。

EC拡張テーブル
抽象構文	解釈（ECの値）
complementOf(c)	O - EC(c)
unionOf(c₁ … c_n)	EC(c₁) ∪ … ∪ EC(c_n)
intersectionOf(c₁ … c_n)	EC(c₁) ∩ … ∩ EC(c_n)
oneOf(i₁ … i_n), for i_j individual IDs	{S(i₁), …, S(i_n)}
oneOf(v₁ … v_n), for v_j literals	{S(v₁), …, S(v_n)}
restriction(p x₁ … x_n), for n > 1	EC(restriction(p x₁)) ∩…∩EC(restriction(p x_n))
restriction(p allValuesFrom(r))	{x ∈ O \| <x,y> ∈ ER(p) implies y ∈ EC(r)}
restriction(p someValuesFrom(e))	{x ∈ O \| ∃ <x,y> ∈ ER(p) ∧ y ∈ EC(e)}
restriction(p value(i)), for i an individual ID	{x ∈ O \| <x,S(i)> ∈ ER(p)}
restriction(p value(v)), for v a literal	{x ∈ O \| <x,S(v)> ∈ ER(p)}
restriction(p minCardinality(n))	{x ∈ O \| card({y ∈ O∪LV : <x,y> ∈ ER(p)}) ≥ n}
restriction(p maxCardinality(n))	{x ∈ O \| card({y ∈ O∪LV : <x,y> ∈ ER(p)}) ≤ n}
restriction(p cardinality(n))	{x ∈ O \| card({y ∈ O∪LV : <x,y> ∈ ER(p)}) = n}
Individual(annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)	EC(annotation(p₁ o₁)) ∩ … EC(annotation(p_k o_k)) ∩ EC(c₁) ∩ … ∩ EC(c_m) ∩ EC(pv₁) ∩…∩ EC(pv_n)
Individual(i annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)	{S(i)} ∩ EC(annotation(p₁ o₁)) ∩ … EC(annotation(p_k o_k)) ∩ EC(c₁) ∩ … ∩ EC(c_m) ∩ EC(pv₁) ∩…∩ EC(pv_n)
value(p Individual(…))	{x ∈ O \| ∃ y∈EC(Individual(…)) : <x,y> ∈ ER(p)}
value(p id) for id an individual ID	{x ∈ O \| <x,S(id)> ∈ ER(p) }
value(p v) for v a literal	{x ∈ O \| <x,S(v)> ∈ ER(p) }
annotation(p o) for o a URI reference	{x ∈ R \| <x,S(o)> ∈ ER(p) }
annotation(p Individual(…))	{x ∈ R \| ∃ y ∈ EC(Individual(…)) : <x,y> ∈ ER(p) }

3.3. 公理と事実の解釈

抽象OWLの解釈Iは、公理と事実の解釈テーブルで示されるような、OWLの公理と事実を満たします。テーブルでは、公理と事実のオプション部分は、角括弧（[…]）内で示され、対応するオプションの条件を持ち、これも角括弧内で示されます。

公理と事実の解釈
命令	解釈に関する条件
Class(c [Deprecated] complete annotation(p₁ o₁) … annotation(p_k o_k) descr₁ … descr_n)	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) = EC(descr₁) ∩…∩ EC(descr_n)
Class(c [Deprecated] partial annotation(p₁ o₁) … annotation(p_k o_k) descr₁ … descr_n)	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) ⊆ EC(descr₁) ∩…∩ EC(descr_n)
EnumeratedClass(c [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) i₁ … i_n)	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) = { S(i₁), …, S(i_n) }
Datatype(c [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) )	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) ⊆ LV
DisjointClasses(d₁ … d_n)	EC(d_i) ∩ EC(d_j) = { } for 1 ≤ i < j ≤ n
EquivalentClasses(d₁ … d_n)	EC(d_i) = EC(d_j) for 1 ≤ i < j ≤ n
SubClassOf(d₁ d₂)	EC(d₁) ⊆ EC(d₂)
DatatypeProperty(p [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) super(s₁) … super(s_n) domain(d₁) … domain(d_n) range(r₁) … range(r_n) [Functional])	[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type) ] S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k)) ER(p) ⊆ O×LV ∩ ER(s₁) ∩…∩ ER(s_n) ∩ EC(d₁)×LV ∩…∩ EC(d_n)×LV ∩ O×EC(r₁) ∩…∩ O×EC(r_n) [ER(p) is functional]
ObjectProperty(p [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) super(s₁) … super(s_n) domain(d₁) … domain(d_n) range(r₁) … range(r_n) [inverse(i)] [Symmetric] [Functional] [ InverseFunctional] [Transitive])	[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type)] S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k)) ER(p) ⊆ O×O ∩ ER(s₁) ∩…∩ ER(s_n) ∩ EC(d₁)×O ∩…∩ EC(d_n)×O ∩ O×EC(r₁) ∩…∩ O×EC(r_n) [ER(p) is the inverse of ER(i)] [ER(p) is symmetric] [ER(p) is functional] [ER(p) is inverse functional] [ER(p) is transitive]
AnnotationProperty(p annotation(p₁ o₁) … annotation(p_k o_k))	S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k))
OntologyProperty(p annotation(p₁ o₁) … annotation(p_k o_k))	S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k))
EquivalentProperties(p₁ … p_n)	ER(p_i) = ER(p_j) for 1 ≤ i < j ≤ n
SubPropertyOf(p₁ p₂)	ER(p₁) ⊆ ER(p₂)
SameIndividual(i₁ … i_n)	S(i_j) = S(i_k) for 1 ≤ j < k ≤ n
DifferentIndividuals(i₁ … i_n)	S(i_j) ≠ S(i_k) for 1 ≤ j < k ≤ n
Individual([i] annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)	EC(Individual([i] annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)) is nonempty