この文書は、
An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL (March 2001)
http://www.w3.org/TR/2001/NOTE-daml+oil-axioms-20011218
の翻訳です。

この文書には翻訳上の誤りがあり得ます。
内容の保証はいたしかねますので、必ずW3Cの正式文書を参照してください。


W3C

RDF,RDF-S,DAML+OILの公理的意味論 (March 2001)

W3C Note 18 December 2001

このバージョン:
http://www.w3.org/TR/2001/NOTE-daml+oil-axioms-20011218
最新バージョン:
http://www.w3.org/TR/daml+oil-axioms
著者:
Richard Fikes
Deborah McGuinness

概要

このドキュメントでは, Resource Description Framework (RDF), RDF Schema (RDF-S), DAML+OILで表現された記述から一階の述語計算で表現された論理的理論への写像を明らかにすることにより, これらの言語に対する一つの公理化を提供する. この論文の基本的な主張は, ここで示した写像によって記述から生成された論理的理論は, 記述が意図している意味と論理的に等価である, ということである. RDF,RDF-S,DAML+OILの記述から一階の述語計算への翻訳手段を与えることで, 記述の意図している意味が論理的理論によって明示されるだけでなく, 伝統的な自動定理証明器や問題解決器を使って自動推論することのできる表現が記述から生成される.   例えば, DAML+OILの公理によって, 推論装置は2つのステートメント, 「class 男性と class 女性は disjointWithである」と 「Johnの type は男性である」から, 「Johnの type は女性である」というステートメントが偽であることを推論することができる.

述語計算への写像は, RDF ステートメントを一階の関係文に翻訳する簡単な規則と, 各々の言語の非論理記号(すなわち,関係,関数,定数)の解釈を制限する一階の論理的公理からなる. RDF Schema DAML+OIL はともにRDFに付加された非論理記号の語彙なので, RDFステートメントの翻訳はRDF-SやDAML+OILに対しても同様に十分な能力を持つ.

公理は, ANSI標準として提案されている ANSI Knowledge Interchange Format ( KIF)) を使って書かれる.

公理的意味論はdaml+oilの発展に合わせて更新され, 最新のバージョンは http://www.ksl.stanford.edu/people/dlm/daml-semantics/abstract-axiomatic-semantics.html から利用可能である. ドキュメントに操作上の利便性を加えるために, 2つの付加的なファイルを包含させる: ドキュメントには

を全て含む.

このドキュメントのステータス

このドキュメントは, Lucent Technologiesから World Wide Web Consortium へのサブミッションである ( サブミッション リクエスト , W3C スタッフ コメント 参照).

コメントをRichard Fikes fikes@ksl.stanford.edu とDeborah L. McGuinness dlm@ksl.stanford.edu ,できれば公開アーカイブされる配布リスト www-rdf-logic@w3.org [ アーカイブ ] へ送っていただきたい.

このドキュメントは覚書であり, W3Cが議論のみを目的として利用可能にしたものである. この覚書をW3Cが公表することが, W3CあるいはW3C Teamないし如何なるW3Cメンバーによる保証を示すわけではない. W3Cは,この覚書の準備に関して編集上のいかなる管理も負っていない. このドキュメントは作業中のものであり, 他のドキュメントによっていつでも更新,置き換え,破棄され得る.

現在のW3C技術文書のリストは, テクニカルレポート ページにある.

目次

  1. はじめに
  2. KIF支持定義
  3. RDF
  4. RDF-S
  5. DAML+OIL

1. はじめに

このドキュメントでは, Resource Description Framework (RDF), RDF Schema (RDF-S), DAML+OILで表現された記述から, 一階の述語計算で表現された論理的理論への写像を明らかにすることにより, これらの言語に対する一つの公理化を提供する.   この論文の基本的な主張は, ここで示した写像によって記述から生成された論理的理論は, 記述が意図している意味と論理的に等価である, ということである.

RDF,RDF-S,DAML+OILの記述から一階の述語計算への翻訳手段を与えることで, 記述の意図している意味が論理的理論によって明示されるだけでなく, 伝統的な自動定理証明器や問題解決器を使って自動推論することのできる表現が記述から生成される. 例えば, DAML+OILの公理によって, 推論装置は2つのステートメント, 「class 男性と class 女性は disjointWithである」と 「Johnの type は男性である」から, 「Johnの type は女性である」というステートメントが偽であることを推論することができる.

述語計算への写像は, RDF (http://www.w3.org/TR/REC-rdf-syntax/) ステートメントを一階の関係文に翻訳する簡単な規則と, 各々の言語の非論理記号(すなわち,関係,関数,定数)の解釈を制限する一階の論理的公理からなる. RDF-S (http://www.w3.org/TR/rdf-schema/)と DAML+OIL はともにRDFに付加された非論理記号の語彙なので, RDFステートメントの翻訳はRDF-SやDAML+OILに対しても同様に十分な能力を持つ.

公理は, ANSI標準として提案されている ANSI Knowledge Interchange Format (KIF) (http://logic.stanford.edu/kif/kif.html) を使って書かれる. 公理では, 標準の一階論理構成要素プラスKIF固有の関係と, リストを扱う関数を使う. [1] 解釈領域中のオブジェクトとしてのリストは, RDFコンテナおよび濃度を扱うDAML+OILプロパティを公理化するために必要である.

これらの言語の各々から一階論理への写像は,次のようにして行う: RDF,RDF-S,DAML+OIL記述の集まりと等価であるKIFの論理的理論は, 以下のように生成される:

1.        述語P,主語S,目的語OのRDFステートメント各々を, "(PropertyValue P S O)"の形式のKIF文に翻訳する.

2.        このドキュメントでソース言語(RDF, RDF-S, DAML+OIL)に関連付けた公理を, KIF理論の中に包含させる.

RDF記述のどのような集まりも等価なRDFステートメントの一つの集合に翻訳できるので, RDFの各々の構成物に対する翻訳を明示する必要はないことに注意. したがって,上記の翻訳規則は 全てのRDFを, ゆえに他の2つの言語の いずれ についても同様に, 翻訳するのに十分である.

この公理化は, 結果として得られる論理的理論において, 非論理記号の解釈による束縛を最小にするように設計されている. 特に, 公理は クラスを集合あるいは単項関係と考えて集合論を使うことは要求しないし, プロパティを写像あるいは2項関係と考えることも求めない. そのような束縛は, もし必要ならば結果の論理的理論に加えることができるが, 翻訳するRDF,RDF-S,DAML+OILで意図された意味を表現するのには必要ではない.

公理は, RDFに関する公理がRDF-SやDAML+OILのプロパティやクラスを使わず, RDF-Sに関する公理がRDFのプロパティやクラスは使うがDAML+OILのプロパティやクラスを使わず, DAML+OILの公理がRDFとRDF-S双方のプロパティやクラスを使うという意味で, RDF,RDF-S,DAML+OILの階層を反映するよう設計されている.

このドキュメントには, 公理から推論できる定理を含めた. これらの定理は, 自動推論において公理の利用を容易にすることを意図したものである. それらは,以下のいずれかである. (1) あらゆる知識ベースの中に含まれていることが仮定できるRDFステートメント (2) RDFステートメントをともなうホーン節あるいはアトムとしての評価可能な束縛 (3) アトム(すなわち,RDFステートメントあるいは評価可能な束縛)の連接が偽となることがある,含意. 各定理は, このドキュメントの中で先に出てきた公理から, 証明することができる.

配布リスト www-rdf-logic@w3.org へ投じられたコメントは歓迎する. [2]

ドキュメントのオンライン付録として, 2つの別のKIFファイルが, このドキュメントから自動的に生成される. これらのファイルは, このドキュメントの中のKIF 公理( http://www.ksl.stanford.edu/people/dlm/daml-semantics/kif-axioms-august2001.txt とKIF 定理( http://www.ksl.stanford.edu/people/dlm/daml-semantics/kif-theorems-august2001.txt ) のみを含む.

2. KIF支持定義

RDF,RDF-S,DAML+OIL記述をKIFで表現する際に使う, 以下のKIF関係を定義する

2.1.          PropertyValue

"PropertyValue"は, あらゆる述語P,あらゆる主語S,あらゆる目的語OがKIF関係文 "(PropertyValue P S O)"に翻訳される3項関係である.

2.2.          Type

"Type"は, 述語がプロパティ"type"であるRDFステートメントの,2項関係の略記法である.

 

%% 関係"Type"は, 関係"PropertyValue"がオブジェクト"type" とSとOについて成り立つ時かつその時に限り, オブジェクトSとOに対して成り立つ.

(<=> (Type ?s ?o) (PropertyValue type[3] ?s ?o))[4] [Type 公理 1]

2.3.         FunctionalProperty

関係"FunctionalProperty"は,RDFとRDF-Sのプロパティの公理化で使われる.

 

%% オブジェクトFPは, FPが"Property"型であり, もしオブジェクトV1とV2がともにあるオブジェクトのFPの値であるならばV1とV2が等しい時かつその時に限り, "FunctionalProperty"型である. (すなわち,ファンクショナル・プロパティは値が関数的であるようなプロパティである)

(<=> (FunctionalProperty ?fp)

     (and (Type ?fp Property)

          (forall (?s ?v1 ?v2)

                  (=> (and (PropertyValue ?fp ?s ?v1)

                           (PropertyValue ?fp ?s ?v2))

                      (= ?v1 ?v2))))) [FunctionalProperty 公理 1]

2.4.          DisjointAll

関係DisjointAllは, DAML+OILのプロパティ"disjointWith"の公理化で使われる.

 

%% オブジェクトLは, Lが"List"型であり, Lがプロパティ"first"の値Fとプロパティ"rest"の値Rを持つならばFがRの"item"の全ての値Cと素であるとともにRが"DisjointAll"である時かつその時に限り, "DisjointAll"である. (すなわち, リストLは要素のあらゆる組み合わせが互いに素である時かつそのときに限り, "DisjointAll"である)

(<=> (DisjointAll ?l)

     (and (Type ?l List)

          (or (= ?l nil)

              (forall (?f ?r)

                      (=> (and (PropertyValue first ?l ?f)

                               (PropertyValue rest ?l ?r))

                          (and (forall (?c)

                                       (=> (PropertyValue item ?r ?c)

                                           (PropertyValue

                                               disjointWith ?f ?c)))

                                (DisjointAll

                                   ?r))))))) [DisjointAll 公理 1]

2.5.          NoRepeatsList

関係NoRepeatsListは, DAML+OILのプロパティ"cardinality", "minCardinality", "maxCardinality"の公理化で使われる.

 

%% "NoRepeatsList"は, 全ての要素が1回しか出現しないリストである.

(<=> (NoRepeatsList ?l)

     (or (= ?l nil)

         (exists (?x) (= ?l (listof ?x)))

         (and (not (item (rest ?l) (first ?l)))

              (NoRepeatsList (rest ?l)))))[5] [NoRepeatsList 公理 1]

3. RDF

はじめにで述べたように, 述語P,主語S,目的語OのRDFステートメントは"(PropertyValue P S O)"の形のKIF文に翻訳される.

この節で定義されるクラスとプロパティのデフォルト名前空間は, http://www.w3.org/1999/02/22-rdf-syntax-ns である.

3.1.          Classes

この節ではRDFに含まれるクラスを公理化する.

3.1.1.       Resource

RDF式で記述される全てのものは,リソースと呼ばれる.

 

%% "Resource"は"Class"型である.

(Type Resource rdfs:Class) [Resource 公理 1]

3.1.2.       Property

 

%% 関係"PropertyValue"の第1引数は"Property"型である

(=> (PropertyValue ?p ?s ?o) (Type ?p Property)) [6] [Property 公理 1]

3.1.3.      rdfs:Class

このクラスは, "rdfs"を前置して名前空間 http://www.w3.org/2000/01/rdf-schema からのものであることを示し, DAML+OILで定義される"Class"からは区別する.

 

%% "Property"型であると同時に"rdfs:Class"型であるオブジェクトは存在しない (すなわち,プロパティとRDF-Sのクラスは互いに素である).

(not (and (Type ?x Property) (Type ?x rdfs:Class))) [rdfs:Class 公理 1]

3.1.4.      Literal

 

%% "Literal"は"rdfd:Class"型である

(Type Literal rdfs:Class)     [Literal 公理 1]

3.1.5.      Statement

 

%% もしオブジェクトSTが"Statement"型ならば, STに対して"Predicate"の値,"Subject"の値,"Object"の値が存在する. (すなわち,全てのステートメントは述語,主語,目的語を持つ)

(=> (Type ?st Statement)

     (exists (?p ?r ?o)

             (and (PropertyValue predicate ?st ?p)

                  (PropertyValue subject ?st ?r)

                  (PropertyValue object ?st ?o)))) [Statement 公理 1]

3.1.6.       Container, Bag, Seq, and Alt

 

%% オブジェクトCが"Container"型ならば, CはKIFリストである. (すなわち,コンテナはKIFで定義されたリストであるとみなされる)

(=> (Type ?c Container) (List ?c)) [Container 公理 1]

 

%% オブジェクトCは, Cが"Bag"型または"Seq"型または"Alt"型である時かつその時に限り, "Container"型である. (すなわち,コンテナは,バッグ,列,またはalternativeである)

(<=> (Type ?c Container)

      (or (Type ?c Bag) (Type ?c Seq) (Type ?c Alt))) [Container 公理 2]

3.1.7.       ContainerMembershipProperty

 

%% もしオブジェクトCが"ContainerMembershipProperty"型ならば, Cは同時に"Property"型である. (すなわち,コンテナ・メンバーシップ・プロパティはプロパティである)

(=> (Type ?c ContainerMembershipProperty)

     (Type ?c Property)) [ContainerMembershipProperty 公理 1]

3.2.          Properties

この節では,RDFに含まれているプロパティを公理化する.

3.2.1.       type

"type"は,リソースがクラスのメンバであることを示すために使われる.

 

%% "type"は"Property"型である.    (すなわち,"type"はプロパティである)

(Type type Property) [type 公理 1]

 

%% "Type"の第1引数はリソースであり,"Type"の第2引数はクラスである.

(=> (Type ?r ?c)

    (and (Type ?r Resource) (Type ?c rdfs:Class))) [7]     [type 公理 2]

 

%% 前出の公理から,以下が推論できることに注意:

(=> (Type ?p Property) (Type ?p Resource)) [8]       [type 定理 1]

(=> (Type ?c rdfs:Class) (Type ?c Resource))        [type 定理 2]

(=> (Type ?s Statement) (Type ?s Resource))        [type 定理 3]

(=> (Type ?c Container) (Type ?c Resource))        [type 定理 4]

(Type Property rdfs:Class)        [type 定理 5]

3.2.2.       subject

 

%% "Subject"は"FunctionalProperty"型であり, オブジェクトSBがオブジェクトSTに対する"Subject"の値ならば, STは"Statement"型でありかつSBは"Resource"型である.    (すなわち,全てのステートメントはただ1個の主語を持ち, その主語はリソースである)

(FunctionalProperty subject)     [subject 公理 1]

(=> (PropertyValue subject ?st ?sb)

     (and (Type ?st Statement) (Type ?sb Resource)))     [subject 公理 2]

3.2.3.       predicate

 

%% "Predicate"は"FunctionalProperty"であり, もしオブジェクトPがオブジェクトSTに対する"Predicate"の値ならば, Pは"Property"型でありかつSTは"Statement"型である.    (すなわち,全てのステートメントはただ1つの述語を持ち,その述語はプロパティである)

(FunctionalProperty predicate) [predicate 公理 1]

(=> (PropertyValue predicate ?st ?p)

     (and (Type ?st Statement) (Type ?p Property))) [predicate 公理 2]

3.2.4.       object

 

%% "Object"は"FunctionalProperty"であり, もしオブジェクトOがオブジェクトSTに対する"Object"の値ならば, Oは"Resource"型であり, STはステートメント型である.    (すなわち,全てのステートメントはただ1つの目的語を持ち, その目的語はリソースである)

(FunctionalProperty object)      [object 公理 1]

(=> (PropertyValue object ?st ?o)

     (and (Type ?st Statement) (Type ?o Resource)))      [object 公理 2]

3.2.5.       value

 

%% "value"は"Property"型であり, もしオブジェクトVがオブジェクトSVに対する"value"の値ならば, SVは"Resource"型であり, Vは"Resource"型である.

(Type value Property) [value 公理 1]

(=> (PropertyValue value ?sv ?v)

     (and (Type ?sv Resource) (Type ?v Resource))) [value 公理 2]

3.2.6.       _1, _2, _3,...

 

%% 全ての正整数Nについて, "_N"は"FunctionalProperty"であり, もしオブジェクトOがオブジェクトCに対する"_N"の値ならば, Cは"Container"型である.    (コンテナにおける_Nの意図は,そのコンテナのN番目の要素である)

(FunctionalProperty _1) [_N 公理 1]

(=> (PropertyValue _1 ?c ?o) (Type ?c Container)) [_N 公理 2]

 

_2, _3, 等についても同様.

4. RDF-S

RDF-Sは, RDFに加えられたクラスとプロパティの集まりである.    RDF-SのステートメントはRDFステートメントである.   

この節で定義されたクラスとプロパティのデフォルト名前空間は, http://www.w3.org/2000/01/rdf-schema である.

4.1.          Classes

この節ではRDF-SでRDFに加えられたクラスを公理化する.

4.1.1.       ConstraintResource

 

%% "ConstraintResource"に対する"subClassOf"の値は"Resource"である.    (すなわち,コンストレイント・リソースはリソースである)

(PropertyValue

    subClassOf ConstraintResource Resource) [ConstraintResource 公理 1]

4.1.2.      ConstraintProperty

 

%% オブジェクトCPは, "ConstraintResource"型かつ"Property"型である時かつその時に限り, "ConstraintProperty"型である.    (すなわち,コンストレイント・プロパティはコンストレイント・リソースのうちプロパティでもあるものである)

(<=> (Type ?cp ConstraintProperty)

      (and (Type ?cp ConstraintResource)

           (Type ?cp Property))) [ConstraintProperty 公理 1]

4.1.3.       NonNegativeInteger

 

%% "NonNegativeInteger"型のオブジェクトは整数である.

(=> (Type ?n NonNegativeInteger)

     (Integer ?n)) [NonNegativeInteger 公理 1]

4.2.          Properties

この節では,RDF-SでRDFに加えられたプロパティを公理化する.

4.2.1.       subClassOf

 

%% "subClassOf"は"Property"型である.

(Type subClassOf Property) [subClassOf 公理 1]

 

%% オブジェクトCSUPERは, CSUPERが"rdfs:Class"型であり, CSUBが"rdfs:Class"型であり, CSUBがCSUPERではなく, もしオブジェクトXがCSUB型ならば同時にCSUPER型である時かつその時に限り, オブジェクトCSUBに対する"subClassOf"の値である.    (すなわち,subClassOfの引数はクラスであり, サブクラスの中のオブジェクトは同時にスーパークラスの中のオブジェクトでもある)

(<=> (PropertyValue subClassOf ?csub ?csuper)

      (and (Type ?csub rdfs:Class)

           (Type ?csuper rdfs:Class)

           (forall (?x) (=> (Type ?x ?csub)

                            (Type ?x ?csuper))))) [subClassOf 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue subClassOf Property Resource) [subClassOf 定理 1]

(PropertyValue subClassOf rdfs:Class Resource) [subClassOf 定理 2]

(PropertyValue subClassOf Statement Resource) [subClassOf 定理 3]

(PropertyValue subClassOf Bag Container) [subClassOf 定理 4]

(PropertyValue subClassOf Seq Container) [subClassOf 定理 5]

(PropertyValue subClassOf Alt Container) [subClassOf 定理 6]

(PropertyValue subClassOf

                ContainerMembershipProperty

                Property) [subClassOf 定理 7]

(=> (and (PropertyValue subClassOf ?csub ?csuper)

          (Type ?x ?csub))

     (Type ?x ?csuper)) [subClassOf 定理 8]

   

4.2.2.       subPropertyOf

 

%% オブジェクトSUPERは, オブジェクトSUBPが"Property"型かつSUPERが"Property"型かつ, もしオブジェクトOに対するSUBPの値がVならばVはOに対するSUPERの値でもある時かつその時に限り, SUBPに対する"subPropertyOf"の値である.    (すなわち,オブジェクトOに対してサブ・プロパティが値Vを持つならば, Oに対してスーパー・プロパティもまた値Vを持つ)

(<=> (PropertyValue subPropertyOf ?subP ?superP)

      (and (Type ?subP Property)

           (Type ?superP Property)

           (forall (?o ?v)

                   (=> (PropertyValue ?subP ?o ?v)

                       (PropertyValue

                          ?superP ?o ?v))))) [subPropertyOf 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(=> (and (PropertyValue subPropertyOf ?subP ?superP)

          (PropertyValue ?subP ?o ?v))

     (PropertyValue ?superP ?o ?v)) [subPropertyOf 定理 1]

4.2.3.       seeAlso

 

%% "seeAlso"に対する"domain"と"range"の値はともに"Resource"である.    (すなわち,"seeAlso"は引数がリソースであるプロパティである)

(PropertyValue domain seeAlso Resource)     [seeAlso 公理 1]

(PropertyValue range seeAlso Resource)     [seeAlso 公理 2]

4.2.4.       isDefinedBy

 

%% "isDefinedBy"に対する"subProperty"の値は"seeAlso"である.    (すなわち,"isDefinedBy"は"seeAlso"のサブ・プロパティである)

(PropertyValue subPropertyOf isDefinedBy seeAlso) [isDefinedBy 公理 1]

4.2.5.       comment

 

%% "comment"に対する"range"の値は"Literal"である.    (すなわち,"comment"は値がリテラルであるプロパティである)

(PropertyValue range comment Literal)     [comment 公理 1]

4.2.6.       label

 

%% "label"に対する"range"の値は"Literal"である.    (すなわち,"label"は値がリテラルであるプロパティである)

(PropertyValue range label Literal) [label 公理 1]

4.3.          Constraint Properties

 

%% "ConstraintProperty"に対する"subClassOf"の値は"Property"である.    (すなわち,コンストレイント・プロパティはプロパティである)

(PropertyValue

    subClassOf ConstraintProperty Property) [ConstraintProperty 公理 1]

4.3.1.       range

 

%% "range"は"ConstraintProperty"型であり"FunctionProperty"型である

(Type range ConstraintProperty) [range 公理 1]

(FunctionalProperty range) [range 公理 2]

 

%% オブジェクトRは, オブジェクトPが"Property"型であり, Rが"rdfs:Class"型であり, もしオブジェクトYがPの値であるならばYがR型である時かつその時に限り, Pに対する"range"の値である.    (すなわち,Pがプロパティ,Rがクラス,Pの全ての値がRの一つである時,RはPのレンジである)

(<=> (PropertyValue range ?p ?r)

      (and (Type ?p Property)

           (Type ?r rdfs:Class)

           (forall (?x ?y) (=> (PropertyValue ?p ?x ?y)

                               (Type ?y ?r))))) [range 公理 3]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue range subClassOf rdfs:Class)       [range 定理 1]

(PropertyValue range range rdfs:Class)       [range 定理 2]

(PropertyValue range type rdfs:Class)       [range 定理 3]

(PropertyValue range subject Resource)      

(PropertyValue range predicate Property)       [range 定理 5]

(PropertyValue range object Resource)       [range 定理 6]

(PropertyValue range subPropertyOf Property)       [range 定理 7]

(=> (and (PropertyValue range ?p ?r)

          (PropertyValue ?p ?x ?y))

     (Type ?y ?r)) [range 定理 8]

4.3.2.       domain

 

%% "domain"は"ConstraintProperty"型である.

(Type domain ConstraintProperty)     [domain 公理 1]

 

%% オブジェクトPに対する"domain"の値がオブジェクトDならば, Pは"Property"型で, Dは"rdfs:Class"型で, もしPがオブジェクトXに対する値を持つならばXはD型である.    (すなわち,DがPのドメインならば,Pはプロパティ,Dはクラス,Pの値を持つ全てのオブジェクトはDの一つである)

(<=> (PropertyValue domain ?p ?d)

      (and (Type ?p Property)

           (Type ?d rdfs:Class)

           (forall (?x ?y) (=> (PropertyValue ?p ?x ?y)

                               (Type ?x ?d)))))      [domain 公理 2]

 

%% 上記の公理から,以下が推論されることに注意:

(PropertyValue domain domain Property)      [domain 定理 1]

(PropertyValue range domain rdfs:Class)      [domain 定理 2]

(PropertyValue domain type Resource)      [domain 定理 3]

(PropertyValue domain subject Statement)      [domain 定理 4]

(PropertyValue domain predicate Statement)      [domain 定理 5]

(PropertyValue domain object Statement)      [domain 定理 6]

(PropertyValue domain subClassOf rdfs:Class)      [domain 定理 7]

(PropertyValue domain range Property)      [domain 定理 8]

(PropertyValue domain subPropertyOf Property)      [domain 定理 9]

(=> (and (PropertyValue domain ?p ?d)

          (PropertyValue ?p ?x ?y))

     (Type ?x ?d)) [domain 定理 10]

(PropertyValue domain value Resource)      [domain 定理 11]

 

%% 全ての正整数iに対して:

(PropertyValue domain _i Container)      [domain 定理 11+i]

5. DAML+OIL

DAML+OILは, RDFとRDF-Sに加えられたクラス,プロパティ,オブジェクトの集まりである.   DAML+OILのステートメントはRDFステートメントである.   

この節で定義されたクラスとプロパティのデフォルト名前空間は, http://www.w3.org/2000/01/rdf-schema である.

5.1.          Classes

この節では,RDFとRDF-Sに加えられたクラスを公理化する.

5.1.1.       Class

 

%% "Class"は"rdfs:Class"のサブクラスである.

(PropertyValue subClassOf Class rdfs:Class) [class 公理 1]

5.1.2.       Datatype

 

%% "Datatype"は"rdfs:Class"のサブクラスである.

(PropertyValue subClassOf Datatype rdfs:Class)   [Datatype 公理 1]

5.1.3.       Thing

 

%% "Thing"は"Class"型である.

(Type Thing Class) [Thing 公理 1]

 

%% 全てのオブジェクトXは"Thing"型である.    (すなわち,"Thing"は全てのオブジェクトのクラスである)

(Type ?x Thing) [Thing 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(=> (Type Class ?c)

      (PropertyValue subClassOf ?c Thing))       [Thing 定理 1]

5.1.4.       Nothing

 

%% "Nothing"は"Thing"に対する"complementOf"の値である.   (すなわち,"Nothing"は"Thing"の補元である)

(PropertyValue complementOf Thing Nothing)     [Nothing 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(=> (Type ?x Nothing) FALSE)     [Nothing 定理 1]

5.1.5.       Restriction

 

%% "Restriction"は"Class"のサブクラスである.

(PropertyValue subClassOf Restriction Class) [Restriction 公理 1]

5.1.6.       AbstractProperty

 

%% "Restriction"は"Class"のサブクラスである.

(PropertyValue

    subClassOf AbstractProperty Property) [AbstractProperty 公理 1]

5.1.7.       DatatypeProperty

 

%% "Restriction"は"Class"のサブクラスである.

(PropertyValue

    subClassOf DatatypeProperty Class) [DatatypeProperty 公理 1]

5.1.8.       TransitiveProperty

 

%% オブジェクトPは, Pが"AbstractProperty"型であり, もしオブジェクトXに対するPの値がオブジェクトYでありYに対するPの値がZならばXに対するPの値がZである時かつその時に限り, "TransitiveProperty"型である.

(<=> (Type ?p TransitiveProperty)

      (and (Type ?p AbstractProperty)

           (forall (?x ?y ?z)

                   (=> (and (PropertyValue ?p ?x ?y)

                            (PropertyValue ?p ?y ?z))

                       (PropertyValue

                          ?p ?x ?z))))) [TransitiveProperty 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue subClassOf

               TransitiveProperty

                AbstractProperty) [TransitiveProperty 定理 1]

   

(Type subClassOf TransitiveProperty) [TransitiveProperty 定理 2]

(Type subPropertyOf TransitiveProperty) [TransitiveProperty 定理 3]

(=> (and (Type ?p TransitiveProperty)

          (PropertyValue ?p ?x ?y)

          (PropertyValue ?p ?y ?z))

     (PropertyValue ?p ?x ?z)) [TransitiveProperty 定理 4]

5.1.9.       UniqueProperty

 

%% オブジェクトPは, Pが"Property"型で,かつ もしオブジェクトXに対するPの値がオブジェクトYでかつXに対するPの値がZであるならばYとZは等しい(すなわち,YとZが同じオブジェクト)時, かつその時に限って, "UniqueProperty"型である.

(<=> (Type ?p UniqueProperty)

      (and (Type ?p Property)

           (forall (?x ?y ?z) (=> (and (PropertyValue ?p ?x ?y)

                                      (PropertyValue ?p ?x ?z))

                                 (= ?y ?z))))) [UniqueProperty 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue

    subClassOf UniqueProperty Property) [UniqueProperty 定理 1]

(Type predicate UniqueProperty) [UniqueProperty 定理 1]

(Type subject UniqueProperty) [UniqueProperty 定理 2]

(Type object UniqueProperty [UniqueProperty 定理 3]

(Type range UniqueProperty) [UniqueProperty 定理 4]

 

%% 全ての正整数iに対して:

(Type _i UniqueProperty) [UniqueProperty 定理 6]

5.1.10.   UnambiguousProperty

 

%% オブジェクトPは, Pが"AbstractPropery"型で, オブジェクトXに対するPの値がオブジェクトVでかつオブジェクトYに対するPの値がVであるならばXとYが等しい(すなわち,XとYが同じオブジェクトである)時かつその時に限り, "UnambiguousProperty"型である.

(<=> (Type ?p UnambiguousProperty)

      (and (Type ?p AbstractProperty)

           (forall (?x ?y ?v)

                   (=> (and (PropertyValue ?p ?x ?v)

                            (PropertyValue ?p ?y ?v))

                       (= ?x ?y))))) [UnambiguousProperty 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue subClassOf

               UnambiguousProperty

                AbstractProperty) [UnambiguousProperty 定理 1]

5.1.11.   List

 

%% "Seq"は"List"に対する"subClassOf"の値である.    (すなわち,リストは列である)

(PropertyValue subClassOf List Seq) [List 公理 1]

5.1.12.   Ontology

 

%% オントロジは"Class"型である.

(Type Ontology Class)    [Ontology 公理 1]

5.2.          Properties

この節では, RDFとRDF-Sに加えられたプロパティを公理化する.

5.2.1.       equivalentTo

 

%% オブジェクトYは, オブジェクトXがYと等しい時かつその時に限り, Xに対する"equivalentTo"の値である.    (すなわち,XとYが"equivalentTo"であることと, XとYが同じオブジェクトを示すことは,論理的に等価である)

(<=> (PropertyValue equivalentTo ?x ?y)

      (= ?x ?y)) [equivalentTo 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue

    inverseOf equivalentTo equivalentTo) [equivalentTo 定理 1]

(Type TransitiveProperty equivalentTo) [equivalentTo 定理 2]

(=> (Type ?x Thing)

     (PropertyValue equivalentTo ?x ?x)) [equivalentTo 定理 3]

(=> (and (PropertyValue equivalentTo ?x ?y) (Type ?x ?c))

     (Type ?y ?c)) [equivalentTo 定理 4]

(=> (and (Type ?p UniqueProperty)

          (PropertyValue ?p ?x ?y)

          (PropertyValue ?p ?x ?z))

     (PropertyValue equivalentTo ?y ?z)) [equivalentTo 定理 5]

(=> (and (Type ?p UnambiguousProperty)

          (PropertyValue ?p ?x ?v)

          (PropertyValue ?p ?y ?v))

     (PropertyValue equivalentTo ?x ?y)) [equivalentTo 定理 6]

5.2.2.       sameClassAs

 

%% "equivalentTo"は, "sameClassAs"に対する"subPropertyOf"の値である.    (すなわち,"sameClassAs"はクラスに対する"equivalentTo"である)

(PropertyValue

    subPropertyOf sameClassAs equivalentTo) [sameClassAs 公理 1]

 

%% C2は, C2がC1に対する"subClassOf"の値であり, かつC1がC2に対する"subClassOf"の値であるときかつその時に限り, C1に対する"sameClassAs"の値である.

(<=> (PropertyValue sameClassAs ?c1 ?c2)

      (and (subClassOf ?c1 ?c2)

           (subClassOf ?c2 ?c1))) [sameClassAs 公理 2]

 

%% C1が"Class"型であり, かつC2がC1に対する"equivalentTo"の値ならば, C2はC1に対する"sameClassAs"の値である.    (すなわち, もしC1がクラスでC2と等しければ,C1はC2にsameClassAsである)

(=> (and (Type ?c1 Class)

          (PropertyValue equivalentTo ?c1 ?c2))

     (PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs 公理 3]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue

    subPropertyOf sameClassAs subClassOf) [sameClassAs 定理 1]

(=> (and (PropertyValue subClassOf ?c1 ?c2)

          (PropertyValue subClassOf ?c2 ?c1))

     (PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs 定理 2]

(=> (and (PropertyValue equivalentTo ?c1 ?c2)

          (Type ?c1 Class))

     (PropertyValue sameClassAs ?c1 ?c2)) [sameClassAs 定理 3]

5.2.3.       samePropertyAs

 

%% "equivalentTo"は, "samePropertyAs"に対する"subPropertyOf"の値である.    (すなわち,"samePropertyAs"はプロパティに対する"equivalentTo"である)

(PropertyValue

    subPropertyOf samePropertyAs equivalentTo) [samePropertyAs 公理 1]

 

%% P2がP1に対する"subPropertyOf"の値であり, P1がP2に対する"subPropertyOf"の値であるときかつその時に限り, P2はP1に対する"samePropertyAs"の値である.

(<=> (PropertyValue samePropertyAs ?P1 ?P2)

      (and (subPropertyOf ?P1 ?P2)

           (subPropertyOf ?P2 ?P1))) [samePropertyAs 公理 2]

 

%% P1が"Property"型であり, P2がP1に対する"equivalentTo"の値ならば, P2はP1に対する"samePropertyAs"の値である. (すなわち,P1がプロパティであり,P1とP2が等しければ, P1はP2にsamePropertyAsである)

(=> (and (Type ?P1 Property)

          (PropertyValue equivalentTo ?P1 ?P2))

     (PropertyValue samePropertyAs ?P1 ?P2)) [samePropertyAs 公理 3]

 

%% "samePropertyAs"と"subPropertyOf"の公理から,以下が推論できることに注意:

(PropertyValue subPropertyOf

                 samePropertyAs

                subPropertyOf) [samePropertyAs 定理 1]

(PropertyValue

    inverseOf samePropertyAs samePropertyAs) [samePropertyAs 定理 2]

(=> (and (PropertyValue subPropertyOf ?p1 ?p2)

          (PropertyValue subPropertyOf ?p2 ?p1))

     (PropertyValue samePropertyAs ?p1 ?p2)) [samePropertyAs 定理 3]

(=> (and (PropertyValue equivalentTo ?p1 ?p2)

          (Type ?p1 Property))

     (PropertyValue samePropertyAs ?p1 ?p2)) [samePropertyAs 定理 4]

5.2.4.       disjointWith

 

%% "disjointWith"は"Property"型である.

(Type disjointWith Property) [disjointWith 公理 1]

 

%% オブジェクトC2は, オブジェクトC1が"Class"型であり, C2が"Class"型であり, C1型で同時にC2型であるオブジェクトXが存在しない時かつその時に限り, C1に対する"disjointWith"の値である.

(<=> (PropertyValue disjointWith ?c1 ?c2)

      (and (Type ?c1 Class)

           (Type ?c2 Class)

           (not (exists (?x)

                        (and (Type ?x ?c1)

                            (Type ?x ?c2)))))) [disjointWith 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue domain disjointWith Class) [disjointWith 定理 1]

(PropertyValue

    inverseOf disjointWith disjointWith) [disjointWith 定理 2]

(PropertyValue disjointWith Property rdfs:Class) [disjointWith 定理 3]

(=> (and (PropertyValue disjointWith ?c1 ?c2)

          (Type ?x ?c1)

          (Type ?x ?c2))

     FALSE) [disjointWith 定理 4]

(=> (and (PropertyValue disjointWith ?c1 ?c2)

          (PropertyValue subClassOf ?c ?c1))

     (PropertyValue disjointWith ?c ?c2)) [disjointWith 定理 5]

(=> (and (PropertyValue disjointWith ?c1 ?c2)

          (PropertyValue subClassOf ?c ?c1)

          (PropertyValue subClassOf ?c ?c2))

     (PropertyValue sameClassAs ?c Nothing)) [disjointWith 定理 6]

5.2.5.       unionOf

 

%% オブジェクトLがオブジェクトC1に対する"unionOf"の値ならば, C1は"Class"型,Lは"List"型, リストLの全ての要素は"Class"型であり, C1型のオブジェクトはリストLの1つ以上のクラスの型のオブジェクトである.

(=> (PropertyValue unionOf ?c1 ?l)

     (and (Type ?c1 Class)

          (Type ?l List)

          (forall (?x) (=> (PropertyValue item ?x ?l) (Type ?x Class)))

          (forall (?x)

                  (<=> (Type ?x ?c1)

                       (exists (?c2)

                                (and (PropertyValue item ?c2 ?l)

                                   (Type ?x ?c2)))))))     [unionOf 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue domain unionOf Class)     [unionOf 定理 1]

(PropertyValue range unionOf List)     [unionOf 定理 2]

(=> (and (PropertyValue unionOf ?c1 ?l)

          (PropertyValue unionOf ?c2 ?l))

     (PropertyValue sameClassAs ?c1 ?c2))     [unionOf 定理 3]

5.2.6.       disjointUnionOf

 

%% オブジェクトLは, LがオブジェクトCに対する"unionOf"の値であり, Lが"DisjointAll"である時かつその時に限り, Cに対する"disjointUnionOf"の値である.   (すなわち,オブジェクトCは, Lがペアワイズ・ディスジョイント・クラスのリストであり, CがクラスのリストLの和であるとき, かつその時に限って, オブジェクトLの直和である)

(<=> (PropertyValue disjointUnionOf ?c ?l)

      (and (PropertyValue unionOf ?c ?l)

           (DisjointAll ?l))) [disjointUnionOf 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue

    subPropertyOf disjointUnionOf unionOf) [disjointUnionOf 定理 1]

5.2.7.       intersectionOf

 

%% オブジェクトLは, オブジェクトC1が"Class"型であり, Lが"List"型であり, リストLの全ての要素が"Class"型であり, C1型のオブジェクトがリストLの全てのクラスを型とするオブジェクトである時かつその時に限り, C1の"intersectionOf"の値である.

(<=> (PropertyValue intersectionOf ?c1 ?l)

      (and (Type ?c1 Class)

           (Type ?l List)

           (forall (?c) (=> (PropertyValue item ?l ?c) (Type ?c Class)))

           (forall (?x)

                   (<=> (Type ?x ?c1)

                        (forall

                          (?c2)

                          (=> (PropertyValue item ?l ?c2)

                              (Type

                               ?x ?c2))))))) [intersectionOf 公理 1]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue domain intersectionOf Class) [intersectionOf 定理 1]

(PropertyValue range intersectionOf List) [intersectionOf 定理 2]

5.2.8.       complementOf

 

%% オブジェクトC2は, オブジェクトC1とC2がディスジョイントクラスであり, 全てのオブジェクトがC1型またはC2型である時かつその時に限り, C1に対する"complementOf"の値である.

(<=> (PropertyValue complementOf ?c1 ?c2)

      (and (PropertyValue disjointWith ?c1 ?c2)

           (forall (?x) (or (Type ?x ?c1)

                             (Type ?x ?c2))))) [complementOf 公理 1]

 

(=> (and (PropertyValue complementOf ?c ?r)

          (PropertyValue onProperty ?r ?p)

          (PropertyValue hasValue ?r ?v))

     (<=> (not (PropertyValue ?p ?o ?v))

          (Type ?o ?c))) [complementOf 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue

    subPropertyOf complementOf disjointWith) [complementOf 定理 1]

(PropertyValue

    inverseOf complementOf complementOf) [complementOf 定理 2]

(=> (and (PropertyValue complementOf ?c1 ?c2)

          (PropertyValue disjointWith ?c1 ?c3))

     (PropertyValue subClassOf ?c3 ?c2)) [complementOf 定理 3]

(=> (and (PropertyValue complementOf ?c1 ?c2)

          (PropertyValue complementOf ?c3 ?c4)

           (PropertyValue subClassOf ?c1 ?c3))

     (PropertyValue subClassOf ?c4 ?c2)) [complementOf 定理 4]

5.2.9.       oneOf

 

%% オブジェクトLは, オブジェクトCが"Class"型であり, Lが"List"型であり, C型のオブジェクトがLに対する"item"の値であるオブジェクトと一致する時かつその時に限り, Cに対する"oneOf"の値である.    (すなわち,CがLの"oneOf"であることは, Cがクラスであり,Lがリストであり,C型のオブジェクトはリストL上のオブジェクトであることである)

(<=> (PropertyValue oneOf ?c ?l)

      (and (Type ?c Class)

           (Type ?l List)

           (forall (?x)

                   (<=> (Type ?x ?c)

                       (PropertyValue item ?l ?x))))) [oneOf 公理 1]

 

%% 上記の公理から,以下が推論されることに注意:

(PropertyValue domain oneOf Class)       [oneOf 定理 1]

(PropertyValue range oneOf List)       [oneOf 定理 2]

(=> (and (PropertyValue oneOf ?c1 ?l)

          (PropertyValue oneOf ?c2 ?l))

     (PropertyValue sameClassAs ?c1 ?c2))       [oneOf 定理 3]

5.2.10.   onProperty

 

%% "onProperty"に対する"domain"の値は"Restriction"である.   (すなわち, onPropertyの第1引数はリストリクションである)

(PropertyValue domain onProperty Restriction) [onProperty 公理 1]

 

%% "onProperty"に対する"range"の値は"Property"である.   (すなわち,onPropertyの第2引数はプロパティである)

(PropertyValue range onProperty Property) [onProperty 公理 2]

5.2.11.   toClass

 

%% "toClass"に対する"domain"の値は"Restriction"である.   (すなわち,toClassの第1引数はリストリクションである)

(PropertyValue domain toClass Restriction)    [toClass 公理 1]

 

%% "toClass"に対する"range"の値は,"rdfs:Class"である.   (すなわち,toClassの第2引数はクラスである)

(PropertyValue range toClass rdfs:Class)     [toClass 公理 2]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値でありかつクラスCがRに対する"toClass"の値ならば, Iに対するPの全ての値がC型である時かつその時に限りオブジェクトIはR型である.    (すなわち, プロパティPに関するCの"toClass"リストリクションは, オブジェクトIに対するPの全ての値がC型になる全てのIの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue toClass ?r ?c))

     (forall (?i) (<=> (Type ?i ?r)

                       (forall (?j)

                               (=> (PropertyValue ?p ?i ?j)

                                  (Type ?j ?c))))))     [toClass 公理 3]

 

%% 上記の公理から,以下が推論されることに注意:

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue toClass ?r ?c)

          (Type ?x ?r)

          (PropertyValue ?p ?x ?v))

     (Type ?v ?c))     [toClass 定理 1]

(=> (and (PropertyValue onProperty ?r1 ?p)

          (PropertyValue toClass ?r1 ?c1)

          (PropertyValue onProperty ?r2 ?p)

          (PropertyValue toClass ?r2 ?c2)

          (PropertyValue subClassOf ?c1 ?c2))

     (PropertyValue subClassOf ?r1 ?r2))     [toClass 定理 2]

(=> (and (PropertyValue onProperty ?r1 ?p)

          (PropertyValue toClass ?r1 ?c1)

          (PropertyValue onProperty ?r2 ?p)

          (PropertyValue toClass ?r2 ?c2)

          (PropertyValue disjointWith ?c1 ?c2))

     (PropertyValue disjointWith ?r1 ?r2))     [toClass 定理 3]

5.2.12.   hasValue

 

%% "hasValue"に対する"domain"の値は,"Restriction"である.   (すなわち,hasValueの第1引数はリストリクションである)

(PropertyValue domain hasValue Restriction)    [hasValue 公理 1]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値でありかつオブジェクトVがRに対する"hasValue"の値ならば, VがオブジェクトIに対するPの値である時かつその時に限り, IはR型である.    (すなわち,プロパティPに関するVの"hasValue"リストリクションは, Pの値としてVを持つ全てのオブジェクトの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue hasValue ?r ?v))

     (forall (?i) (<=> (Type ?i ?r)

                      (PropertyValue ?p ?i ?v))))    [hasValue 公理 2]

 

%% 上記の公理から,以下が推論されることに注意:

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue hasValue ?r ?v)

          (Type ?i ?r))

     (PropertyValue ?p ?i ?v))    [hasValue 定理 1]

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue hasValue ?r ?v)

          (PropertyValue ?p ?i ?v))

     (Type ?i ?r))    [hasValue 定理 2]

5.2.13.   hasClass

 

%% "hasClass"に対する"domain"の値は"Restriction"である.   (すなわち,hasClassの第1引数はリストリクションである)

(PropertyValue domain hasClass Restriction)    [hasClass 公理 1]

 

%% "hasClass"に対する"range"の値は,"rdfs:Class"である.   (すなわち,hasClassの第2引数はクラスである)

(PropertyValue range hasClass rdfs:Class)   [hasClass 公理 2]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値であり, Rに対する"hasClass"の値がクラスCならば, オブジェクトXに対するPの値Vが存在しXが"Type"の値としてCを持つ時かつその時に限り, RはXに対する"Type"の値である.    (すなわち,プロパティPに関するCの"hasClass"リストリクションは, C型のPの値を持つ全てのオブジェクトの集まりである)

(=> (and (PropertyValue hasClass ?r ?c)

          (PropertyValue onProperty ?r ?p))

     (forall (?x)

             (<=> (Type ?x ?r)

                  (exists (?v) (and (PropertyValue ?p ?x ?v)

                                   (Type ?v ?c))))))    [hasClass 公理 3]

 

%% 上記の公理より,以下が推論されることに注意:

(=> (and (PropertyValue hasClass ?r ?c)

          (PropertyValue onProperty ?r ?p)

          (PropertyValue ?p ?x ?v)

          (Type ?v ?c))

     (Type ?x ?r))    [hasClass 定理 1]

5.2.14.   minCardinality

 

%% "minCardinality"に対する"domain"の値は"Restriction"である.   (すなわち,minCardinalityの第1引数はリストリクションである)

(PropertyValue

    domain minCardinality Restriction) [minCardinality 公理 1]

 

%% "minCardinality"に対する"range"の値は"nonNegativeInteger"である.   (すなわち,minCardinalityの第2引数は非負整数である)

(PropertyValue

    range minCardinality NonNegativeInteger) [minCardinality 公理 2]

 

%% プロパティPがリストリクションRに対する"onProperty"の値でありかつ非負整数NがRに対する"minCardinality"の値であるならば, 全ての要素がオブジェクトIに対するPの値である長さN以上の"NoRepeatsList"が存在する時かつその時に限り, IはR型である.   (すなわち,プロパティPに関するNの"minCardinality"リストリクションは, Pの値を少なくともN個持つ全てのオブジェクトIのクラスである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue minCardinality ?r ?n))

     (forall (?i)

             (<=> (Type ?i ?r)

                  (exists (?vl)

                          (and (NoRepeatsList ?vl)

                               (forall (?v)

                                 (=> (PropertyValue item ?vl ?v)

                                    (PropertyValue ?p ?i ?v)))

                               (>= (length ?vl)

                                  ?n)))))) [9] [minCardinality 公理 3]

5.2.15.   maxCardinality

 

%% "maxCardinality"に対する"domain"の値は"Restriction"である.   (すなわち,maxCardinalityの第1引数はリストリクションである)

(PropertyValue

    domain maxCardinality Restriction) [maxCardinality 公理 1]

 

%% "maxCardinality"に対する"range"の値は"NonNegativeInteger"である.    (すなわち,maxCardinalityの第2引数は非負整数である)

(PropertyValue

    range maxCardinality NonNegativeInteger) [maxCardinality 公理 2]

 

%% プロパティPがリストリクションRに対する"onProperty"の値でありかつRに対する"maxCardinality"の値が非負整数Nであるならば, 要素がPの値と一致する全ての"NoRepeatsLists"がN以下の長さを持つ時かつその時に限り, IはR型である.    (すなわち,プロパティPに関するNの"maxCardinality"リストリクションは, PのたかだかN個の値を持つ全てのオブジェクトIの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue maxCardinality ?r ?n))

     (forall (?i)

             (<=> (Type ?i ?r)

                  (forall (?vl)

                          (=> (and (NoRepeatsList ?vl)

                                   (forall (?v)

                                            (<=> (PropertyValue

                                                 item ?vl ?v)

                                               (PropertyValue

                                                 ?p ?i ?v))))

                              (=< (length ?vl)

                                 ?n)))))) [10] [maxCardinality 公理 3]

5.2.16.   cardinality

 

%% "cardinality"に対する"domain"の値は"Restriction"である.   (すなわち,cardinalityの第1引数はリストリクションである)

(PropertyValue domain cardinality Restriction) [cardinality 公理 1]

 

%% "cardinality"に対する"range"の値は"NonNegativeInteger"である.    (すなわち,cardinalityの第2引数は非負整数である)

(PropertyValue

    range cardinality NonNegativeInteger) [cardinality 公理 2]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値であり, 非負整数NがRに対する"cardinality"の値ならば, 要素がPの値と一致する全ての"NoRepeatsLists"の長さがNである時かつその時に限り, オブジェクトIはR型である.    (すなわち,プロパティPに関するNの"cardinality"リストリクションは, ちょうどN個のPの値を持つ全てのオブジェクトIの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue cardinality ?r ?n))

     (forall (?i) (<=> (Type ?i ?r)

                       (forall (?vl)

                               (=> (and (NoRepeatsList ?vl)

                                        (forall

                                          (?v)

                                         (<=> (PropertyValue

                                                  item ?vl ?v)

                                              (PropertyValue

                                                ?p ?i ?v))))

                                   (= (length ?vl)

                                     ?n)))))) [cardinality 公理 3]

5.2.17.   hasClassQ

 

%% "hasClassQ"に対する"domain"の値は"Restriction"である.   (すなわち,hasClassQの第1引数はリストリクションである)

(PropertyValue domain hasClassQ Restriction) [hasClassQ 公理 1]

 

%% "hasClassQ"に対する"range"の値は"rdfs:Class"である.    (すなわち,hasClassQの第2引数はクラスである)

(PropertyValue range hasClassQ rdfs:Class) [hasClassQ 公理 2]

5.2.18.   minCardinalityQ

 

%% "minCardinalityQ"に対する"domain"の値は"Restriction"である.   (すなわち,minCardinalityQの第1引数はリストリクションである)

(PropertyValue

    domain minCardinalityQ Restriction) [minCardinalityQ 公理 1]

 

%% "minCardinalityQ"に対する"range"の値は"NonNegativeInteger"である.    (すなわち,minCardinalityQの第2引数は非負整数である)

(PropertyValue

    range minCardinalityQ NonNegativeInteger) [minCardinalityQ 公理 2]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値であり, 非負整数NがRに対する"minCardinalityQ"の値であり, クラスCがRに対する"hasClassQ"の値であるならば, 全ての要素がオブジェクトIに対するPの値かつC型で長さがN以上の"NoRepeatsList"がある時かつその時に限り, IはR型である.    (すなわち,プロパティPに関するNの"minCardinalityQ"リストリクションは, 少なくともN個のC型のPの値を持つ全てのオブジェクトIの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue minCardinalityQ ?r ?n)

          (PropertyValue hasClassQ ?r ?c))

     (forall (?i)

             (<=> (Type ?i ?r)

                  (exists

                     (?vl)

                    (and (NoRepeatsList ?vl)

                         (forall (?v) (=> (PropertyValue item ?vl ?v)

                                          (and (PropertyValue ?p ?i ?v)

                                              (Type ?v ?c))))

                         (>= (length ?vl)

                            ?n)))))) [minCardinalityQ 公理 3]

 

%%上記の公理から,以下が推論できることに注意:

(=> (and (PropertyValue minCardinality ?r1 ?n)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue minCardinalityQ ?r2 ?n)

         (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 Thing))

     (PropertyValue sameClassAs ?r1 ?r2)) [minCardinalityQ 定理 1]

(=> (and (PropertyValue hasValue ?r1 ?v)

          (PropertyValue onProperty ?r1 ?p)

          (Type ?v ?c)

          (PropertyValue hasClassQ ?r2 ?c)

          (PropertyValue minCardinalityQ ?r2 1)

          (PropertyValue onProperty ?r1 ?p))

     (PropertyValue subClassOf ?r1 ?r2)) [minCardinalityQ 定理 2]

(=> (and (PropertyValue hasClass ?r1 ?c)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue hasClassQ ?r2 ?c)

          (PropertyValue minCardinalityQ ?r2 1))

     (PropertyValue sameClassAs ?r2 ?r1)) [minCardinalityQ 定理 3]

(=> (and (PropertyValue minCardinalityQ ?r1 ?n1)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue hasClassQ ?r1 ?c1)

         (PropertyValue minCardinalityQ ?r2 ?n2)

          (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 ?c2)

          (PropertyValue subClassOf ?c1 ?c2)

          (>= ?n1 ?n2))

     (PropertyValue subClassOf ?r1 ?r2)) [minCardinalityQ 定理 4]

5.2.19.   maxCardinalityQ

 

%%"maxCardinalityQ"に対する"domain"の値は"Restriction"である.   (すなわち,maxCardinalityQの第1引数はリストリクションである)

(PropertyValue

    domain maxCardinalityQ Restriction) [maxCardinalityQ 公理 1]

 

%% "maxCardinalityQに対する"range"の値は"NonNegativeInteger"である)    (すなわち,maxCardinalityQの第2引数は非負整数である)

(PropertyValue

    range maxCardinalityQ NonNegativeInteger) [maxCardinalityQ 公理 2]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値であり, 非負整数NがRに対する"maxCardinalityQ"の値であり, クラスCがRに対する"hasClassQ"の値ならば, 要素がPの値と一致しかつC型である全ての"NoRepeatsLists"の長さがN以下である時かつその時に限り, オブジェクトIはR型である.    (すなわち,プロパティPに関するNのリストリクションは, 最大N個のC型のPの値を持つ全てのオブジェクトIの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue maxCardinalityQ ?r ?n)

          (PropertyValue hasClassQ ?r ?c))

     (forall (?i) (<=> (Type ?i ?r)

                        (forall

                         (?vl)

                         (=> (and (NoRepeatsList ?vl)

                                  (forall

                                    (?v)

                                    (<=> (PropertyValue item ?vl ?v)

                                          (and (PropertyValue ?p ?i ?v)

                                             (Type ?v ?c)))))

                             (=< (length ?vl)

                                ?n)))))) [maxCardinalityQ 公理 3]

 

%% 上記の公理から,以下が推論できることに注意:

(=> (and (PropertyValue maxCardinality ?r1 ?n)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue maxCardinalityQ ?r2 ?n)

          (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 Thing))

     (PropertyValue sameClassAs ?r1 ?r2)) [maxCardinalityQ 定理 1]

(=> (and (PropertyValue minCardinalityQ ?r1 ?n1)

          (PropertyValue onProperty ?r1 ?p)

         (PropertyValue hasClassQ ?r1 ?c1)

          (PropertyValue maxCardinalityQ ?r2 ?n2)

          (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 ?c2)

          (PropertyValue subClassOf ?c1 ?c2)

          (> ?n1 ?n2))

     (PropertyValue disjointWith ?r1 ?r2)) [maxCardinalityQ 定理 2]

(=> (and (PropertyValue maxCardinalityQ ?r 0)

          (PropertyValue onProperty ?r ?p)

          (PropertyValue hasClassQ ?r ?c)

          (Type ?x ?r)

          (PropertyValue ?p ?x ?v)

          (Type ?v ?c))

    FALSE) [maxCardinalityQ 定理 3]

(=> (and (PropertyValue maxCardinalityQ ?r 1)

          (PropertyValue onProperty ?r ?p)

          (PropertyValue hasClassQ ?r ?c)

          (Type ?x ?r)

          (PropertyValue ?p ?x ?v1)

          (Type ?v1 ?c)

          (PropertyValue ?p ?x ?v2)

          (Type ?v2 ?c))

      (PropertyValue equivalentTo ?v1 ?v2)) [maxCardinalityQ 定理 4]

(=> (and (PropertyValue maxCardinalityQ ?r1 ?n1)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue hasClassQ ?r1 ?c1)

          (PropertyValue maxCardinalityQ ?r2 ?n2)

           (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 ?c2)

          (PropertyValue subClassOf ?c2 ?c1)

          (< ?n1 ?n2))

     (PropertyValue subClassOf ?r1 ?r2)) [maxCardinalityQ 定理 5]

5.2.20.   cardinalityQ

 

%% "cardinalityQ"に対する"domain"の値は"Restriction"である.   (すなわち,cardinalityQの第1引数はリストリクションである)

(PropertyValue domain cardinalityQ Restriction) [cardinalityQ 公理 1]

 

%% "cardinalityQ"に対する"range"の値は"NonNegativeInteger"である.    (すなわち,cardinalityQの第2引数は非負整数である)

(PropertyValue

    range cardinalityQ NonNegativeInteger) [cardinalityQ 公理 2]

 

%% もしプロパティPがリストリクションRに対する"onProperty"の値であり, 非負整数NがRに対する"cardinalityQ"の値であり, クラスCがRに対する"hasClassQ"の値ならば, 要素がPの値に一致しかつC型である全ての"NoRepeatsLists"が長さNを持つ時かつその時に限り, IはR型である.    (すなわち,プロパティPに関するNの"cardinalityQ"リストリクションは, N個のC型のPの値を持つ全てのオブジェクトIの集まりである)

(=> (and (PropertyValue onProperty ?r ?p)

          (PropertyValue cardinalityQ ?r ?n)

          (PropertyValue hasClassQ ?r ?c))

     (forall (?i) (<=> (Type ?i ?r)

                       (forall

                         (?vl)

                         (=> (and (NoRepeatsList ?vl)

                                  (forall

                                    (?v)

                                    (<=> (PropertyValue item ?vl ?v)

                                          (and (PropertyValue ?p ?i ?v)

                                             (Type ?v ?c)))))

                             (= (length ?vl)

                               ?n)))))) [cardinalityQ 公理 4]

 

%% 上記の公理から,以下が推論できることに注意:

(=> (and (PropertyValue cardinality ?r1 ?n)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue cardinalityQ ?r2 ?n)

          (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 Thing))

     (PropertyValue sameClassAs ?r1 ?r2)) [cardinalityQ 定理 1]

(=> (and (PropertyValue cardinalityQ ?r1 ?n)

          (PropertyValue onProperty ?r1 ?p)

          (PropertyValue hasClassQ ?r1 ?c)

          (PropertyValue minCardinalityQ ?r2 ?n)

           (PropertyValue onProperty ?r2 ?p)

          (PropertyValue hasClassQ ?r2 ?c)

          (PropertyValue maxCardinalityQ ?r3 ?n)

          (PropertyValue onProperty ?r3 ?p)

          (PropertyValue hasClassQ ?r3 ?c)

          (PropertyValue first ?l1 ?r2)

           (PropertyValue rest ?l1 ?l2)

          (PropertyValue first ?l2 ?r3)

          (PropertyValue rest ?l2 nil))

     (PropertyValue intersectionOf ?r1 ?l1)) [cardinalityQ 定理 2]

5.2.21.   inverseOf

 

%% "inverseOf"は"Property"型である.

(Type inverseOf Property) [inverseOf 公理 1]

 

%% オブジェクトP2は, オブジェクトP1が"AbstractProperty"型であり, P2が"AbstractProperty"型であり, オブジェクトX2がオブジェクトX1に対するP1の値であることとX2に対するP2の値がX1であることが同値である時かつその時に限り, P1に対する"inverseOf"の値である.

(<=> (PropertyValue inverseOf ?p1 ?p2)

      (and (Type ?p1 AbstractProperty)

           (Type ?p2 AbstractProperty)

           (forall (?x1 ?x2)

                   (<=> (PropertyValue ?p1 ?x1 ?x2)

                        (PropertyValue

                          ?p2 ?x2 ?x1))))) [inverseOf 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue domain inverseOf AbstractProperty) [inverseOf 定理 1]

(PropertyValue range inverseOf AbstractProperty) [inverseOf 定理 2]

(=> (and (PropertyValue inverseOf ?p1 ?p2)

          (PropertyValue ?p1 ?x1 ?x2))

     (PropertyValue ?p2 ?x2 ?x1)) [inverseOf 定理 3]

5.2.22.   first

 

%% "first"は"UniqueProperty"型である.

(Type first UniqueProperty)    [first 公理 1]

 

%% オブジェクトXは, オブジェクトLが"List"型でLに対する"_1"の値がXである時かつその時に限り, Lに対する"first"の値である.    (すなわち,"first"はリストに対する"_1"である)

(<=> (PropertyValue first ?l ?x)

      (and (Type ?l List) (PropertyValue _1 ?l ?x))) [first 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue domain first List)       [first 定理 1]

(PropertyValue subPropertyOf first _1)       [first 定理 2]

(=> (and (Type ?l List) (PropertyValue _1 ?l ?x))

     (PropertyValue first ?l ?x)) [first 定理 3]

5.2.23.   rest

 

%% "rest"は"UniqueProperty"型である.

(Type rest UniqueProperty)     [rest 公理 1]

 

%% オブジェクトRは, オブジェクトLが"List"型でありかつRが"List"型であり, LがリストRと同じ要素を同じ順番で持ちさらに先頭に付加的な1要素を持っている時かつその時に限り, Lに対する"rest"の値である.

(<=> (PropertyValue rest ?l ?r)

      (and (Type ?l List)

           (Type ?r List)

           (exists (?x) (= ?l (cons ?x ?r))))) [11] [rest 公理 2]

 

%% "rest"に関する公理から,以下が推論できることに注意:

(PropertyValue domain rest List)        [rest 定理 1]

(PropertyValue range rest List)        [rest 定理 2]

(Type rest uniqueProperty)     [rest 定理 3]

 

%% 全ての正整数Nに対して,以下が推論できる:

(=> (and (PropertyValue rest ?l ?r)

          (PropertyValue _N ?r ?x))

     (PropertyValue _N+1 ?l ?x))    [rest 定理 3+N]

5.2.24.   item

 

%% "item"は"Property"型である.

(Type item Property) [item 公理 1]

 

%% オブジェクトXは, オブジェクトLが"List"型で, XがLに対する"first"の値であるかあるいはLの"rest"の値に対する"item"の値である時かつその時に限り, Lに対する"item"の値である.    (すなわち,XがLの要素であることは, XがリストLの最初の要素であるか, XがリストRの要素となるリストLの残余のRが存在することである)

(<=> (PropertyValue item ?l ?x)

      (and (Type ?l List)

           (or (PropertyValue first ?l ?x)

               (exists (?r)

                       (and (PropertyValue rest ?l ?r)

                            (PropertyValue

                             item ?r ?x)))))) [item 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(PropertyValue domain item List)        [item 定理 1]

(=> (and (PropertyValue unionOf ?c ?l)

          (PropertyValue item ?l ?c1))

     (PropertyValue subClassOf ?c1 ?c))        [item 定理 2]

(=> (and (PropertyValue intersectionOf ?c ?l)

          (PropertyValue item ?l ?c1))

     (PropertyValue subClassOf ?c ?c1))        [item 定理 3]

(=> (and (PropertyValue oneOf ?c ?l)

          (Type ?x ?c))

     (PropertyValue item ?l ?x)) [item 定理 4]

(=> (and (PropertyValue oneOf ?c ?l)

          (PropertyValue item ?l ?x))

     (Type ?x ?c)) [item 定理 5]

(=> (and (PropertyValue rest ?l ?r)

          (PropertyValue item ?r ?x))

     (PropertyValue item ?l ?x))    [item 定理 6]

(PropertyValue subPropertyOf first item) [item 定理 7]

 

%% 全ての正整数Nに対して,以下が推論できる:

(=> (and (Type ?l List)

          (PropertyValue _N ?l ?x))

     (PropertyValue item ?l ?x))    [item 定理 7+N]

5.2.25.   versionInfo

 

%% "versionInfo"はプロパティである.

(Type versionInfo Property) [versionInfo 公理 1]

5.2.26.   imports

 

%% "imports"はプロパティである.

(Type imports Property)     [imports 公理 1]

5.3.          Other Objects

5.3.1.       nil

 

%% "nil"は,"item"の値を持たないリストである.   (すなわち,"nil"は空リストである)

(Type nil List)    [nil 公理 1]

(not (PropertyValue item nil ?x))     [nil 公理 2]

 

%% 上記の公理から,以下が推論できることに注意:

(=> (PropertyValue first nil ?x) FALSE) [nil 定理 1]

(=> (PropertyValue rest nil ?x) FALSE) [nil 定理 2]

 



[1] このドキュメントの以前のバージョンでは, "holds"や列変数のような, 他の一階論理言語にはない付加的なKIF構成要素を用いていた.    このバージョンでは, そのような構成要素は公理化から除いた.

[2] このドキュメントの初期バージョンのデバッグにおける, Pat Hayes,Peter Patel-Schneider,Richard Waldingerの惜しみない助力に感謝する.    また, Ken Baclawski,Alex Borgida,Dan Connolly,Ora LassilaをはじめRDFメイリングリストからの建設的なコメントに感謝する.

[3] typeについてより詳しくは3.2.1節を参照.

[4] KIF note:    "<=>"は"if and only if"を意味する.    KIFでは関係文は"(<relation name> <argument>*)"の形式を取る.    最初の文字が ``?'' の名前は変数である.    限定作用素(quantifier)が陽に示されない時は, 変数には全称作用素が与えられているとする.

[5] KIF notes: "nil"は空リストを表す.    "(listof x)"は, 最初の(かつ唯一の)要素がxである長さ1のリストを示す句である.    "="は「解釈領域において同一のオブジェクトを示す」ことを意味する.    "item"は, 第2引数で示されたオブジェクトが第1引数で示されたリストの要素であるとき成立する2項関係である.    "first"は, 引数で示されたリストの第1要素を値とする単項関数である.   "rest"は引数が空でないリストのとき値を持ち, その値は引数に示されたリストの第1要素を除く全ての要素からなるリストである, 単項関数である.

[6] KIF note:    "=>"は"implies"を意味する.

[7] プロパティ"domain"と"range"はRDF-Sで定義されるプロパティなので, RDFの公理では使わない.

[8] プロパティ"subClassOf"はRDF-Sで定義されるプロパティなので, RDFの公理では使わない.

[9] KIF note: "length"は"length"の引数に示されたリストの中にある要素の数を示すKIF関数であり, ">="は「大きいかまたは等しい」を表すKIF関係である.

[10] KIF note: "=<"は「小さいかまたは等しい」を表すKIF関係である.

[11] KIF note: "cons"はオブジェクトとリストを引数とし, オブジェクトをリストの第1要素となるよう付加して作ったリストが関数の値となるKIF関数である.