この文書は， A Model-Theoretic Semantics for DAML+OIL (March 2001) の翻訳です．
この文書には翻訳上の誤りがあり得ます． 内容の保証はいたしかねますので， 必ずW3Cの正式文書を参照してください．
(c)2001 Frank van Harmelen , [ Ian Horrocks], and Lucent Technologies, Inc. . All Rights Reserved. Distribution policies are governed by the W3C intellectual property terms .
DAML+OIL構文の意味は， この簡潔なモデル理論セマンティクスによって与えられる．
このドキュメントは， Lucent Technologiesから World Wide Web Consortium へのサブミッションである （ サブミッション リクエスト , W3C スタッフ コメント 参照）．
コメントをPeter F. Patel-Schneider pfps@research.bell-labs.com ，できれば公開アーカイブされる配布リスト www-rdf-logic@w3.org [ アーカイブ ] へ送っていただきたい．
このドキュメントは覚書であり， W3Cが議論のみを目的として利用可能にしたものである． この覚書をW3Cが公表することが， W3CあるいはW3C Teamないし如何なるW3Cメンバーによる保証を示すわけではない． W3Cは，この覚書の準備に関して編集上のいかなる管理も負っていない． このドキュメントは作業中のものであり， 他のドキュメントによっていつでも更新，置き換え，破棄され得る．
現在のW3C技術文書のリストは， テクニカルレポート ページにある．
このドキュメントは，DAML+OILのモデル理論セマンティクスの簡潔な仕様を与える． DAML+OILオントロジ（あるいは知識ベース）はRDF３項組の集まりである． これらの３項組の中には， DAML+OILに関係するものとそうでないものがある． このセマンティクスでは，DAML+OILに明白に関係する３項組のみを扱い， それ以外のものは無視する．
このドキュメントでは， RDF３項組の集まりがどのようにして獲得されるかには触れない． また， ネーミングとインポートのあらゆる側面も無視する． したがって， OntologyやversionInfo，importsの意味は扱わない． （importsが意図する意味は， 参照されたオントロジのRDF３項組を， 現在のオントロジのRDF３項組が含むことである）
このドキュメントでは，集合や集合関係その他の数学的表記を表すために， 様々な表示上の便法を使う． これらは最もエレガントな便法ではないかもしれないが， ほとんど全てのHTMLブラウザで表示することができる．
このドキュメント中の名前のうち，DAML+OIL名前空間以外の名前空間からのものは修飾する． 以下のXML名前空間の定義が存在するものと仮定する：
いくつかのDAML+OIL構文は， リストを受け入れる． 簡潔さと明瞭さのため， 意味写像ではリストを[x1,...,xn]と表す．
意味論は，DAML+OILオブジェクトの集まりである空でない解釈領域， AD，を用いる． このオブジェクト領域に， データ型領域DDを加える． DDはXML Schemaデータ型の意図モデルであり， 他の値の無限の集まりとは疎に合併する． ADとDDの直和を，UDと表す．
意味論は，３つの解釈関数によって，様々な構文要素に意味を与える：
DAML+OILオントロジのいくつかのノードは，XML Schema データ型定義である． そのようなノードは，ICによってデータ型ドメインの適切な部分集合に写像される． （あるノードがXML Schema データ型定義かどうか知るためには， それがXML Schemaの文脈の中にあるかどうかを調べれば良い． XML Schema組み込みデータ型に対しては，標準URIからも知ることができる） daml:Classのインスタンスであるノードは， ICによってオブジェクト領域ADの部分集合に写像される． 特別な場合として，rdfs:LiteralはICによってDDに写像される．
写像IRは，オブジェクトプロパティをAD x ADの部分集合に， データ型プロパティをAD x DDの部分集合に写像する．
写像IOは，RDFリテラルをDDの部分集合に写像する． この部分集合は， XML Schema データ型の字句表現としてそのリテラルを持つ， 全てのDDの要素を含んでいなければならない． また， XML Schema データ型の解釈の中にあり， XML Schema データ型の字句表現としてリテラルを持たない， DDの要素を含んではならない． XML Schema データ型を型とするノードは， そのXML Schema データ型の写像の部分集合に写像される． 他の全てのノードは，ADの１要素部分集合に写像される．
現在のところ，名前の唯一性に関する仮定はない． 個体の同等性あるいは非同等性を決定する方法は助けになるだろう． （実際，２つの個体が同じか異なっているかを示すクラスを作ることによってこれは行えるだろうが， 直接的な方法の方が良い）
構文構造から意味構造上の束縛への写像を通じて， 意味論を明らかにする． ほとんどの写像は仮引数を持つ． 仮引数は``?''を前置することで示す． 写像には，数個の３項組の関与を要求するものもある．
RDF３項組の集まりの形式のDAML+OILオントロジを考える． 意味構造<AD,IC,IO,IR>は， オントロジからの写像の結果得られる束縛がその構造の中で真であるならば， DAML+OILオントロジのモデルである．
最初に，いくつかの前提となる写像を導入する． これらの写像の効果のいくつかは， 上の意味構造の構成と構文ドキュメントの定義から生じるが， 強調のためここに含める．
| 構文構造 | 意味束縛 |
|---|---|
| <rdf:type,?C,rdfs:Class> | IC(?C) <= UD |
| <rdf:type,?C,Class> | IC(?C) <= AD |
| <rdf:type,?C,Datatype> | IC(?C) <= DD |
| <rdf:type,?C,Restriction> | IC(?C) <= AD |
| <rdf:type,?R,Property> | IR(?R) <= AD x UD |
| <rdf:type,?R,ObjectProperty> | IR(?R) <= AD x AD |
| <rdf:type,?R,DatatypeProperty> | IR(?R) <= AD x DD |
| IC(Thing) = AD | |
| IC(Nothing) = { } | |
| IC(rdfs:Literal) = DD | |
| ?L | リテラル?L に対して， IO(?L) <= DDかつ， もしXML Schemaデータ型の解釈の中にxがあるならば， xがXML Schemaデータ型の字句表現として?Lを持つ時かつその時に限り， x in IO(?L) |
次に，実際の意味写像について．
| 構文構造 | 意味束縛 |
|---|---|
| <rdf:type,?O,?C> | IO(?O) <= IC(?C) |
| <rdf:type,?O,?D> <rdf:value,?O,?L> <rdf:type,?L,rdfs:Literal> | XML Schemaデータ型?Dに対して， 字句表現?Lを持つIC(?D)の要素が一つあれば， IO(?O)はその要素を含む１要素集合であり， そうでなければIO(?O) = { } |
| <?R,?O1,?O2> | あるx <=IO(?O1)とy <= IO(?O2)に対して， IO(?O1) <= ADならば， <x,y> in IR(?R) |
| <equivalentTo,?A,?B> | IC(?A) = IC(?B) IR(?A) = IR(?B) IO(?A) = IO(?B) |
| <rdfs:subClassOf,?C,?D> | IC(?C) <= IC(?D) |
| <rdfs:subPropertyOf,?R,?S> | IR(?R) <= IR(?S) |
| <sameClassAs,?C,?D> | IC(?C) = IC(?D) |
| <samePropertyAs,?R,?S> | IR(?R) = IR(?S) |
| <sameIndividualAs,?A,?B> | IO(?A) = IO(?B) |
| <disjointWith,?X,?Y> | IC(?X) ^ IC(?Y) = { } |
| <differentIndividualFrom,?A,?B> | IO(?A) ^ IO(?B) = { } |
| <unionOf,?C,[?X1,...,?Xn]> | IC(?C) = ( IC(?X1) v ... v IC(?Xn) ) ^ AD |
| <disjointUnionOf,?C,[?X1,...,?Xn]> | IC(?C) = ( IC(?X1) v ... v IC(?Xn) ) ^ AD |
| 1<=i<j<=nに対して， IC(?Xi) ^ IC(?Xj) = { } | |
| <intersectionOf,?C,[?X1,...,?Xn]> | IC(?C) = IC(?X1) ^ ... ^ IC(?Xn) ^ AD |
| <complementOf,?X,?Y> | IC(?X) ^ IC(?Y) = { } |
| IC(?X) v IC(?Y) = AD | |
| <oneOf,?C,[?O1,...,?On]> | IC(?C) = ( IO(?O1) v ... v IO(?On) ) ^ AD |
| <rdfs:domain,?P,?C> | <x,y> in IR(?P)ならば，x in IC(?C) |
| <rdfs:range,?P,?C> | <x,y> in IR(?P)ならば，y in IC(?C) |
| <inverseOf,?P,?S> | y in ADに対して， <x,y> in IR(?P) iff <y,x> in IR(?S) |
| <rdf:type,?P,TransitiveProperty> | y in ADに対して， もし<x,y> in IR(?P)かつ<y,z> in IR(?P)ならば， <x,z> in IR(?P) |
| <rdf:type,?P,UniqueProperty> | もし<x,y> in IR(?P)かつ<x,z> in IR(?P)ならば， y=z |
| <rdf:type,?P,UnambiguousProperty> | y in ADに対して， もし<x,y> in IR(?P)かつ<z,y> in IR(?P)ならば， x=z |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <toClass,?R,?C> | x in IC(?R) iff IR(?P)({x}) <= IC(?C) |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <hasValue,?R,?V> | x in IC(?R) iff | IR(?P)({x}) ^ IO(?V) | > 0 |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <hasClass,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0 |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <minCardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | >= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <maxCardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | <= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <cardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | = ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,ObjectProperty> <cardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <toClass,?R,?C> | x in IC(?R) iff IR(?P)({x}) <= IC(?C) |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <hasValue,?R,?V> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?V) | > 0 |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <hasClass,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | > 0 |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <minCardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | >= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <maxCardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | <= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <cardinality,?R,?n> | x in IC(?R) iff | IR(?P)({x}) | = ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <minCardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | >= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <maxCardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | <= ?n |
| <rdf:type,?R,Restriction> <onProperty,?R,?P> <rdf:type,?P,DatatypeProperty> <cardinalityQ,?R,?n> <hasClassQ,?R,?C> | x in IC(?R) iff | IR(?P)({x}) ^ IC(?C) | = ?n |