この文書は、
An Axiomatic Semantics for RDF, RDF-S, and DAML+OIL (March 2001)
http://www.w3.org/TR/2001/NOTE-daml+oil-axioms-20011218
の翻訳です。
この文書には翻訳上の誤りがあり得ます。
内容の保証はいたしかねますので、必ずW3Cの正式文書を参照してください。
(c)2001 Richard Fikes and Deborah L. McGuinness . All Rights Reserved. Distribution policies are governed by the W3C intellectual property terms .
このドキュメントでは， Resource Description Framework (RDF), RDF Schema (RDF-S), DAML+OILで表現された記述から一階の述語計算で表現された論理的理論への写像を明らかにすることにより， これらの言語に対する一つの公理化を提供する． この論文の基本的な主張は， ここで示した写像によって記述から生成された論理的理論は， 記述が意図している意味と論理的に等価である， ということである． RDF，RDF-S，DAML+OILの記述から一階の述語計算への翻訳手段を与えることで， 記述の意図している意味が論理的理論によって明示されるだけでなく， 伝統的な自動定理証明器や問題解決器を使って自動推論することのできる表現が記述から生成される． 例えば， DAML+OILの公理によって， 推論装置は２つのステートメント， 「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 から利用可能である． ドキュメントに操作上の利便性を加えるために， ２つの付加的なファイルを包含させる： ドキュメントには
を全て含む．
このドキュメントは， 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技術文書のリストは， テクニカルレポート ページにある．
このドキュメントでは， Resource Description Framework (RDF), RDF Schema (RDF-S), DAML+OILで表現された記述から， 一階の述語計算で表現された論理的理論への写像を明らかにすることにより， これらの言語に対する一つの公理化を提供する． この論文の基本的な主張は， ここで示した写像によって記述から生成された論理的理論は， 記述が意図している意味と論理的に等価である， ということである．
RDF，RDF-S，DAML+OILの記述から一階の述語計算への翻訳手段を与えることで， 記述の意図している意味が論理的理論によって明示されるだけでなく， 伝統的な自動定理証明器や問題解決器を使って自動推論することのできる表現が記述から生成される． 例えば， DAML+OILの公理によって， 推論装置は２つのステートメント， 「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を， ゆえに他の２つの言語の いずれ についても同様に， 翻訳するのに十分である．
この公理化は， 結果として得られる論理的理論において， 非論理記号の解釈による束縛を最小にするように設計されている． 特に， 公理は クラスを集合あるいは単項関係と考えて集合論を使うことは要求しないし， プロパティを写像あるいは２項関係と考えることも求めない． そのような束縛は， もし必要ならば結果の論理的理論に加えることができるが， 翻訳する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]
ドキュメントのオンライン付録として， ２つの別の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 ） のみを含む．
RDF，RDF-S，DAML+OIL記述をKIFで表現する際に使う， 以下のKIF関係を定義する
"PropertyValue"は， あらゆる述語P，あらゆる主語S，あらゆる目的語OがKIF関係文 "(PropertyValue P S O)"に翻訳される３項関係である．
"Type"は， 述語がプロパティ"type"であるRDFステートメントの，２項関係の略記法である．
%% 関係"Type"は， 関係"PropertyValue"がオブジェクト"type" とSとOについて成り立つ時かつその時に限り， オブジェクトSとOに対して成り立つ．
(<=> (Type ?s ?o) (PropertyValue type[3] ?s ?o))[4] [Type 公理 1]
関係"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]
関係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]
関係NoRepeatsListは， DAML+OILのプロパティ"cardinality", "minCardinality", "maxCardinality"の公理化で使われる．
%% "NoRepeatsList"は， 全ての要素が１回しか出現しないリストである．
(<=> (NoRepeatsList ?l)
(or (= ?l nil)
(exists (?x) (= ?l (listof ?x)))
(and (not (item (rest ?l) (first ?l)))
(NoRepeatsList (rest ?l)))))[5] [NoRepeatsList 公理 1]
はじめにで述べたように， 述語P，主語S，目的語OのRDFステートメントは"(PropertyValue P S O)"の形のKIF文に翻訳される．
この節で定義されるクラスとプロパティのデフォルト名前空間は， http://www.w3.org/1999/02/22-rdf-syntax-ns である．
この節ではRDFに含まれるクラスを公理化する．
RDF式で記述される全てのものは，リソースと呼ばれる．
%% "Resource"は"Class"型である．
(Type Resource rdfs:Class) [Resource 公理 1]
%% 関係"PropertyValue"の第１引数は"Property"型である
(=> (PropertyValue ?p ?s ?o) (Type ?p Property)) [6] [Property 公理 1]
このクラスは， "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]
%% "Literal"は"rdfd:Class"型である
(Type Literal rdfs:Class) [Literal 公理 1]
%% もしオブジェクト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]
%% オブジェクト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]
%% もしオブジェクトCが"ContainerMembershipProperty"型ならば， Cは同時に"Property"型である． （すなわち，コンテナ・メンバーシップ・プロパティはプロパティである）
(=> (Type ?c ContainerMembershipProperty)
(Type ?c Property)) [ContainerMembershipProperty 公理 1]
この節では，RDFに含まれているプロパティを公理化する．
"type"は，リソースがクラスのメンバであることを示すために使われる．
%% "type"は"Property"型である． （すなわち，"type"はプロパティである）
(Type type Property) [type 公理 1]
%% "Type"の第１引数はリソースであり，"Type"の第２引数はクラスである．
(=> (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]
%% "Subject"は"FunctionalProperty"型であり， オブジェクトSBがオブジェクトSTに対する"Subject"の値ならば， STは"Statement"型でありかつSBは"Resource"型である． （すなわち，全てのステートメントはただ１個の主語を持ち， その主語はリソースである）
(FunctionalProperty subject) [subject 公理 1]
(=> (PropertyValue subject ?st ?sb)
(and (Type ?st Statement) (Type ?sb Resource))) [subject 公理 2]
%% "Predicate"は"FunctionalProperty"であり， もしオブジェクトPがオブジェクトSTに対する"Predicate"の値ならば， Pは"Property"型でありかつSTは"Statement"型である． （すなわち，全てのステートメントはただ１つの述語を持ち，その述語はプロパティである）
(FunctionalProperty predicate) [predicate 公理 1]
(=> (PropertyValue predicate ?st ?p)
(and (Type ?st Statement) (Type ?p Property))) [predicate 公理 2]
%% "Object"は"FunctionalProperty"であり， もしオブジェクトOがオブジェクトSTに対する"Object"の値ならば， Oは"Resource"型であり， STはステートメント型である． （すなわち，全てのステートメントはただ１つの目的語を持ち， その目的語はリソースである）
(FunctionalProperty object) [object 公理 1]
(=> (PropertyValue object ?st ?o)
(and (Type ?st Statement) (Type ?o Resource))) [object 公理 2]
%% "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]
%% 全ての正整数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, 等についても同様．
RDF-Sは， RDFに加えられたクラスとプロパティの集まりである． RDF-SのステートメントはRDFステートメントである．
この節で定義されたクラスとプロパティのデフォルト名前空間は， http://www.w3.org/2000/01/rdf-schema である．
この節ではRDF-SでRDFに加えられたクラスを公理化する．
%% "ConstraintResource"に対する"subClassOf"の値は"Resource"である． （すなわち，コンストレイント・リソースはリソースである）
(PropertyValue
subClassOf ConstraintResource Resource) [ConstraintResource 公理 1]
%% オブジェクトCPは， "ConstraintResource"型かつ"Property"型である時かつその時に限り， "ConstraintProperty"型である． （すなわち，コンストレイント・プロパティはコンストレイント・リソースのうちプロパティでもあるものである）
(<=> (Type ?cp ConstraintProperty)
(and (Type ?cp ConstraintResource)
(Type ?cp Property))) [ConstraintProperty 公理 1]
%% "NonNegativeInteger"型のオブジェクトは整数である．
(=> (Type ?n NonNegativeInteger)
(Integer ?n)) [NonNegativeInteger 公理 1]
この節では，RDF-SでRDFに加えられたプロパティを公理化する．
%% "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]
%% オブジェクト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]
%% "seeAlso"に対する"domain"と"range"の値はともに"Resource"である． （すなわち，"seeAlso"は引数がリソースであるプロパティである）
(PropertyValue domain seeAlso Resource) [seeAlso 公理 1]
(PropertyValue range seeAlso Resource) [seeAlso 公理 2]
%% "isDefinedBy"に対する"subProperty"の値は"seeAlso"である． （すなわち，"isDefinedBy"は"seeAlso"のサブ・プロパティである）
(PropertyValue subPropertyOf isDefinedBy seeAlso) [isDefinedBy 公理 1]
%% "comment"に対する"range"の値は"Literal"である． （すなわち，"comment"は値がリテラルであるプロパティである）
(PropertyValue range comment Literal) [comment 公理 1]
%% "label"に対する"range"の値は"Literal"である． （すなわち，"label"は値がリテラルであるプロパティである）
(PropertyValue range label Literal) [label 公理 1]
%% "ConstraintProperty"に対する"subClassOf"の値は"Property"である． （すなわち，コンストレイント・プロパティはプロパティである）
(PropertyValue
subClassOf ConstraintProperty Property) [ConstraintProperty 公理 1]
%% "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]
%% "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]
DAML+OILは， RDFとRDF-Sに加えられたクラス，プロパティ，オブジェクトの集まりである． DAML+OILのステートメントはRDFステートメントである．
この節で定義されたクラスとプロパティのデフォルト名前空間は， http://www.w3.org/2000/01/rdf-schema である．
この節では，RDFとRDF-Sに加えられたクラスを公理化する．
%% "Class"は"rdfs:Class"のサブクラスである．
(PropertyValue subClassOf Class rdfs:Class) [class 公理 1]
%% "Datatype"は"rdfs:Class"のサブクラスである．
(PropertyValue subClassOf Datatype rdfs:Class) [Datatype 公理 1]
%% "Thing"は"Class"型である．
(Type Thing Class) [Thing 公理 1]
%% 全てのオブジェクトXは"Thing"型である． （すなわち，"Thing"は全てのオブジェクトのクラスである）
(Type ?x Thing) [Thing 公理 2]
%% 上記の公理から，以下が推論できることに注意:
(=> (Type Class ?c)
(PropertyValue subClassOf ?c Thing)) [Thing 定理 1]
%% "Nothing"は"Thing"に対する"complementOf"の値である． （すなわち，"Nothing"は"Thing"の補元である）
(PropertyValue complementOf Thing Nothing) [Nothing 公理 1]
%% 上記の公理から，以下が推論できることに注意:
(=> (Type ?x Nothing) FALSE) [Nothing 定理 1]
%% "Restriction"は"Class"のサブクラスである．
(PropertyValue subClassOf Restriction Class) [Restriction 公理 1]
%% "Restriction"は"Class"のサブクラスである．
(PropertyValue
subClassOf AbstractProperty Property) [AbstractProperty 公理 1]
%% "Restriction"は"Class"のサブクラスである．
(PropertyValue
subClassOf DatatypeProperty Class) [DatatypeProperty 公理 1]
%% オブジェクト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]
%% オブジェクト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]
%% オブジェクト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]
%% "Seq"は"List"に対する"subClassOf"の値である． （すなわち，リストは列である）
(PropertyValue subClassOf List Seq) [List 公理 1]
%% オントロジは"Class"型である．
(Type Ontology Class) [Ontology 公理 1]
この節では， RDFとRDF-Sに加えられたプロパティを公理化する．
%% オブジェクト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]
%% "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]
%% "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]
%% "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]
%% オブジェクトLがオブジェクトC1に対する"unionOf"の値ならば， C1は"Class"型，Lは"List"型， リストLの全ての要素は"Class"型であり， C1型のオブジェクトはリストLの１つ以上のクラスの型のオブジェクトである．
(=> (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]
%% オブジェクト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]
%% オブジェクト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]
%% オブジェクト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]
%% オブジェクト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]
%% "onProperty"に対する"domain"の値は"Restriction"である． （すなわち， onPropertyの第１引数はリストリクションである）
(PropertyValue domain onProperty Restriction) [onProperty 公理 1]
%% "onProperty"に対する"range"の値は"Property"である． （すなわち，onPropertyの第２引数はプロパティである）
(PropertyValue range onProperty Property) [onProperty 公理 2]
%% "toClass"に対する"domain"の値は"Restriction"である． （すなわち，toClassの第１引数はリストリクションである）
(PropertyValue domain toClass Restriction) [toClass 公理 1]
%% "toClass"に対する"range"の値は，"rdfs:Class"である． （すなわち，toClassの第２引数はクラスである）
(PropertyValue range toClass rdfs:Class) [toClass 公理 2]