3. 直接モデル理論セマンティクス(規範)
このOWLのモデル理論セマンティクスは、OWL DL抽象構文(OWL Lite抽象構文を含む)のオントロジーから標準モデル理論へ直接的に展開します。これは、RDFSセマンティクスの語彙拡張である、5項のセマンティクスより単純です。
3.1. 語彙と解釈
ここでは、セマンティクスは、語彙の概念で始まります。OWLオントロジーについて考える場合、語彙は、オントロジーによってインポートされるオントロジーのみならず、すべてのURI参照およびリテラルをそのオントロジーに含んでいなければなりませんが、他のURI参照およびリテラルを含むこともできます。
この項では、VOPは、組み込みOWLオントロジープロパティーに対するURI参照です。
定義: OWL語彙Vは、1組のリテラルVLおよび7組のURI参照、VC、VD、VI、VDP、VIP、VAP、およびVOから成ります。任意の語彙では、VCとVDは互いに素で、VDP、VIP、VAP、およびVOPは、対で互いに素です。VD(語彙のクラス名)は、owl:Thingおよびowl:Nothingを含んでいます。VD(語彙のデータ型名)は、組み込みOWLデータ型およびrdfs:Literalに対するURI参照を含んでいます。VAP(語彙のアノテーション・プロパティー名)は、owl:versionInfo、rdfs:label、rdfs:comment、rdfs:seeAlso、およびrdfs:isDefinedByを含んでいます。VIP(語彙の個体値プロパティー名)、VDP(語彙のデータ値プロパティー名)、およびVI(語彙の個体名)、VO(語彙のオントロジー名)には、既定のメンバーはありません。
定義: RDFと同様に、データ型dは、字句スペースL(d)(1組のUnicode文字列)、値スペースV(d)、および字句スペースから値スペースへのトータル・マッピングL2V(d)を特徴としています。
定義: データ型マップDは、xsd:stringおよびxsd:integerを適切なXMLスキーマ・データ型にマッピングする、URI参照からデータ型への部分的なマッピングです。
データ型マップは、他の組み込みOWLデータ型に対するデータ型を含むことができます。他のデータ型も含むことができますが、OWL構文には、これらのデータ型が何であるかを伝える方法が備わっていません。
定義: Dをデータ型マップとします。以下の場合、語彙VL、VC、VD、VI、VDP、VIP、VAP、VOを持つDに関する抽象OWL解釈は、1組の形式I = <R, EC, ER, L, S, LV>です(Pが、べき集合(power set)演算子である場合)。
- R(Iの資源)が空でない集合
- LV(Iのリテラルの値)が、Unicode文字列の集合、対のUnicode文字列と言語タグの集合、およびDにおける各データ型に対する値スペース、を含んでいるRのサブセット
- EC : VC → P(O)
- EC : VD → P(LV)
- ER : VDP → P(O×LV)
- ER : VIP → P(O×O)
- ER : VAP ∪ { rdf:type } → P(R×R)
- ER : VOP → P(R×R)
- L : TL → LV(TLがVLにおいて型付きリテラルの集合である場合)
- S : VI ∪ VC ∪ VD ∪ VDP ∪
VIP ∪ VAP ∪ VO
∪ { owl:Ontology, owl:DeprecatedClass, owl:DeprecatedProperty }
→ R
- S(VI) ⊆ 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は、リテラルを自身に(本質的に)マッピングすることにより、VLにおいてプレーンなリテラルに拡張されます、つまり、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(c1 … cn) |
EC(c1) ∪ … ∪ EC(cn) |
intersectionOf(c1 … cn) |
EC(c1) ∩ … ∩ EC(cn) |
oneOf(i1 … in),
for ij individual IDs |
{S(i1), …, S(in)} |
oneOf(v1 … vn),
for vj literals |
{S(v1), …, S(vn)} |
restriction(p x1 …
xn), for n > 1 |
EC(restriction(p x1)) ∩…∩EC(restriction(p xn)) |
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(p1 o1) … annotation(pk ok)
type(c1) … type(cm) pv1 … pvn) |
EC(annotation(p1 o1)) ∩ …
EC(annotation(pk ok)) ∩
EC(c1) ∩ … ∩ EC(cm) ∩
EC(pv1) ∩…∩ EC(pvn) |
Individual(i annotation(p1 o1) … annotation(pk ok)
type(c1) … type(cm) pv1 … pvn) |
{S(i)} ∩ EC(annotation(p1 o1)) ∩ …
EC(annotation(pk ok)) ∩
EC(c1) ∩ … ∩ EC(cm) ∩
EC(pv1) ∩…∩ EC(pvn) |
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(p1 o1) … annotation(pk ok)
descr1 … descrn) |
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) …
S(c) ∈ EC(annotation(pk ok))
EC(c) = EC(descr1) ∩…∩ EC(descrn) |
Class(c [Deprecated] partial
annotation(p1 o1) … annotation(pk ok)
descr1 … descrn) |
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) …
S(c) ∈ EC(annotation(pk ok))
EC(c) ⊆ EC(descr1) ∩…∩ EC(descrn) |
EnumeratedClass(c [Deprecated]
annotation(p1 o1) … annotation(pk ok)
i1 … in) |
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) …
S(c) ∈ EC(annotation(pk ok))
EC(c) = { S(i1), …, S(in) } |
Datatype(c [Deprecated]
annotation(p1 o1) … annotation(pk ok) ) |
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p1 o1)) …
S(c) ∈ EC(annotation(pk ok))
EC(c) ⊆ LV |
DisjointClasses(d1 … dn) |
EC(di) ∩ EC(dj) = { } for 1 ≤ i < j ≤ n |
EquivalentClasses(d1 … dn) |
EC(di) = EC(dj) for 1 ≤ i < j ≤ n |
SubClassOf(d1 d2) |
EC(d1) ⊆ EC(d2) |
DatatypeProperty(p [Deprecated]
annotation(p1 o1) … annotation(pk ok)
super(s1) … super(sn)
domain(d1) … domain(dn) range(r1) … range(rn)
[Functional])
|
[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type) ]
S(p) ∈ EC(annotation(p1 o1)) …
S(p) ∈ EC(annotation(pk ok))
ER(p) ⊆ O×LV ∩ ER(s1) ∩…∩ ER(sn) ∩
EC(d1)×LV ∩…∩ EC(dn)×LV ∩ O×EC(r1) ∩…∩ O×EC(rn)
[ER(p) is functional] |
ObjectProperty(p [Deprecated]
annotation(p1 o1) … annotation(pk ok)
super(s1) … super(sn)
domain(d1) … domain(dn) range(r1) … range(rn)
[inverse(i)] [Symmetric]
[Functional] [ InverseFunctional]
[Transitive])
|
[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type)]
S(p) ∈ EC(annotation(p1 o1)) …
S(p) ∈ EC(annotation(pk ok))
ER(p) ⊆ O×O ∩ ER(s1) ∩…∩ ER(sn) ∩
EC(d1)×O ∩…∩ EC(dn)×O ∩ O×EC(r1) ∩…∩ O×EC(rn)
[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(p1 o1) … annotation(pk ok))
|
S(p) ∈ EC(annotation(p1 o1)) …
S(p) ∈ EC(annotation(pk ok)) |
OntologyProperty(p annotation(p1 o1) … annotation(pk ok))
|
S(p) ∈ EC(annotation(p1 o1)) …
S(p) ∈ EC(annotation(pk ok)) |
EquivalentProperties(p1 … pn) |
ER(pi) = ER(pj) for 1 ≤ i < j ≤ n |
SubPropertyOf(p1 p2) |
ER(p1) ⊆ ER(p2) |
SameIndividual(i1 … in) |
S(ij) = S(ik) for 1 ≤ j < k ≤ n |
DifferentIndividuals(i1 … in) | S(ij) ≠ S(ik) for 1 ≤ j < k ≤ n |
Individual([i] annotation(p1 o1) … annotation(pk ok)
type(c1) … type(cm) pv1 … pvn) |
EC(Individual([i] annotation(p1 o1) … annotation(pk ok)
type(c1) … type(cm) pv1 … pvn))
is nonempty |
3.4. オントロジーの解釈
2項で見たように、OWLオントロジーはアノテーションを持つことができ、それは自身のセマンティック条件を必要とします。このローカルの意味のほかに、owl:importsアノテーションは、別のOWLオントロジーの内容を現在のオントロジーにインポートします。インポートされたオントロジーは、あるとすれば、インポート構成子の引数を名前として持っているものです。(このようなインポートの処理は、ウェブの問題とは無縁です。OWLオントロジーの名前の使用は、その名前をウェブ上のオントロジーのロケーションにすることを意図していますが、これはこの形式的な処理の範囲外です。)
定義: Dをデータ型マップとします。抽象OWLの解釈I(VL、VC、VD、VI、VDP、VIP、VAP、VOから成る語彙を持つDに関する)は、以下の場合に限り、OWLオントロジーOを満たします。
- クラスID(データ型ID、個体ID、データ値プロパティーID、個体値プロパティーID、アノテーション・プロパティーID、アノテーションID、オントロジーID)として使用されるOの各URI参照が、VC(それぞれ、VD、VI、VDP、VIP、VAP、VO)に属している、
- Oの各リテラルが、VLに属している、
- Iが、オントロジー・アノテーションを除いて、Oの各命令を満たしている、
- 形式Annotation(p v)の各オントロジー・アノテーションに対し、<o,S(v)> ∈ ER(p)、かつ、Oが名前nを持つ場合にS(n) = oであるような、<o,S(owl:Ontology)> ∈ ER(rdf:type)を持つ、あるo ∈ Rが存在している、そして、
- Iが、Oのowl:importsアノテーション命令で言及された各オントロジーを満たしている。
定義: Iがコレクションにおける各オントロジーおよび公理と事実を満たすような、Dに関するある解釈Iが存在する場合に限り、抽象OWLオントロジーのコレクションおよび公理と事実は、データ型マップDに関して整合性があります。
定義: Oにおいて各オントロジーおよび公理と事実を満たすマップDに関する各解釈がO'も満たす場合、抽象OWLオントロジーのコレクションOおよび公理と事実は、データ型マップDに関する抽象OWLオントロジーあるいは公理か事実O'を、含意(entail)します。