このドキュメントは
Logic and the semantic web
http://www.w3.org/DesignIssues/Logic.html
の和訳です。
この文書には和訳上の誤りがありえます。
内容の保証はいたしかねますので、必ずW3C Webサイトの正式版文書を参照して下さい。

Tim Berners-Lee

Date:
1998, last change:
$Date:
2002/01/11 19:21:31 $ $Author:
connolly $
Status:
personal view only.
Editing status:
first draft.

Up to Design Issues

# The Semantic Web as a language of logic

# ロジックの言語としてのセマンティックWeb

本稿はセマンティックWebデザインを少し形式論理の点から見たものである。形式論理としては、一般のものおよび、特にAccess
Limited Logicシステムを考える。
(訳注：Access-Limited LogicはAlgernonにより作られた体系。http://www.cs.utexas.edu/users/qr/algernon.html
あたりが参考になる）
ここで問題は、私は論理学者でないのに、あまり経験のない領域で宣伝マンのようなことをやらなければならないことである。

## イントロダクション

Semantic Web Toolboxは、Webをロジックのないフラットなデータのリポジトリから、ロジックを表現できるレベルにまで高める手段を論じている。これは従来知識表現システムが行ってきたことである。

セマンティックWebには、クロフォードとKuipersが述べるように、多くの論理システムとは違ったゴールがある[Crawf90]。

[...]知識表現システムには、以下の性質がなければならない:

- 合理的で簡潔なシンタックスがある
- 何を記述しているか正確に言えるよう、厳密に定義されたセマンティクスがある
- 人の知識を表現するのに十分な記述力がある
- 効率的で、強力で、理解可能な推論機構がある
- 大規模知識ベースの構築に利用可能である
しかし、3番目と4番目の性質を同時に達成するのは難しいことが判っている。

セマンティックWebのゴールは、Webが人間間のコミュニケーションに用いられたように、現実の複雑さをできる限り制限なく記述できるようにシステムを統合することである。したがって、3番目の条件は必須である。4番目の条件を削ることで、それは可能である。また、４番目のうち３番目とバッティングするのは「効率的」な推論システムの部分である。

グローバルなセマンティックWebのサブセットで、実際のアプリケーションでは必要のない部分を制限し、適用可能性と効率性を達成するものがあるだろうというのがアイディアである。しかし、セマンティックWeb自体は推論エンジンを規定しない。それは、有効なオペレーションを定義し、それらが一貫していることが必要となる。一般に、セマンティックWebでは、定理の証明をフォローできればよく、証明を作り出す必要はない。

(このKRシステムとセマンティックWebの基本的なゴールの違いは、昔からのハイパーテキストと初期のWebとの違いに似ている。例えば、Webでは柔軟性とスケーラビリティ確保のためにリンク一貫性を落としている。こそのため、個々のウェブサイトで厳密な階層順序やマトリクス構造を使えなくなった。しかしWeb全体としてはそれらは必要ではない。)

もしセマンティックWebマシンがあるとすれば、それは証明チェッカであって、定理証明器ではない。それは、答えを見つけるわけでないし、答えの正当性をチェックするものでもない。しかし、答えが正しいという説明を辿ることはできる。
データソースとしてのセマンティックWebは、様々な推論システムに情報を与えるものではあるが、推論システムそのものではない。

多くの知識表現システムは、推論「ルール」と、信念情報とを区別している。これはしばしば、（式の置き換えのような）ルールは言語内では書けず、言語外で定義されているからである。実際、システムで使われるルールの集合は、しばしばフォーマルに冗長なだけでなく、恣意的である。しかし、セマンティックWebなどのユニバーサルデザインはミニマリズムでないとならない。Webにおける論理的データは直接または間接的にセマンティックWebで書くべきだと強く要望する。それにより、アプリケーションを制限する必要はなくなる。Web上のデータを対象とする異なる機械では、異なるアルゴリズムや異なる推論ルールを使用する。ある場合は、それは強力なAIシステムだし、別の場合は単なる文書変換システムである。重要なのは、いずれのケースでも、同じ基本的で最小のルールに対して、結果が正しくないといけない。実際、証明をやりとりするには、ルールセットは工学的にも選択可能でないといけない。

サブシステムを作成するにあたり、多くの関連する方法がある。

セマンティックWeb言語は、オペレーション、公理、ルールを削ることでサブセット化できること;
ステートメントの集合は特定のドキュメントかウェブサイトからのものに限定できる;
用いられる式の形式は、たとえば文書スキーマを使うことで、制限できる;
アプリケーション設計では、一般の推論エンジンを使った結果が保証されていることで様々な決定が行える
証明は、完全に人手で作られた応用に依存したプログラムで構築される

例えば、Access Limited Logicでは（私が理解する限り）、関係r(a、b)はrがアクセスできる場合にのみ利用可能と制限される。そして、リンクに沿って前向きにのみ推論規則を使用する。また、複雑さを制限するために、ルール集合を分割することでWebを分割化もできる。

セマンティックWebでは概して、扱いやすさが必要とされる。

一貫性、矛盾を導かないこと
すべてのアプリケーションの部分となれるような記述の強力さ

### Grounding in Reality
現実へのグラウンディング

哲学的には、セマンティックWebは、式を操作するのためのルールセット以上のものを生み出す。それはWebの文書が社会的に重要な意味を持っていることを定義する。したがって、単にセマンティックWebを、与えられたシステムの特定の代数と同型になるように制限するだけでは十分ではない。それよりも、特定のシステムが持つWeb表現は、他のセマンティックWebとの連携がマッピングできるように定義できないといけない。電子商取引はこのように堅実な枠組みが必要である。従来電子商取引では、意味は曖昧にしか定義されず、自動処理ができないようなアドホックなシンタックスにより、論理的推論よりも裁判所が決着することが多かった。セマンティックWebを開発することは、電子商取引における用語を定義する堅固な枠組みとなる。

現実には、セマンティックWebのデータの意味は、セマンティックWebと連携する非セマンティックWebアプリケーションで役立つ。例えば、(セマンティックWebを受け付ける)現金振込や電子商取引のアプリケーションでは、現実的には現金振込み装置の様々な用語の意味を定義している。

## Axiomatic Basis
公理的基礎

## 一階論理のレベルでは、同じ結果にたどり着く公理体系のセットが複数ある場合、そのどれかを選択する必要はない。

(A cute one at the propositional logic level seems [Burris,
p126] to be Nicod's set in which nand (in XML toolbox <not>..</not>
and below [xy]) is the Sheffer (sole) connective and the only rules of
inference are substitution and the modus ponens equivelent that
from F and [F[G H]] one can deduce H, and the single axiom [[P[QR]][[S[SS]][[UQ][[PU][PU]]]].)

ここで一階論理の性質を仮定しよう。現在の知識に何かを加える場合、それは一階の組み合わせにより定義され、それによって得られた言語は証明可能な論理システムの部分になっていなければいけない。さもないと、新しいシステム構築には多大な手間がかかる。

## Intractability and Undecidability
複雑性と決定不能性

## セマンティックWebの表現力を増やすために、あまり望ましくはないが２つの目標を設定している。(我々はまだ一貫性を必要としている!)　世界は決定不可能な言明や複雑な問題に満ちている。セマンティックWebはそのようなことがらを表現する能力を持っていなければならない。

CrawfordとKuipersは、同様のことを彼らの「Negation in ALL」という論文の最初で述べている。

「フォーマルに記述された知識表現システムでは、知識の表現力と計算量とはトレードオフの関係にある。」
「例えば、ある知識表現システムが一階述語論理の表現力を持っていたとすると、ｴｰｼﾞｪﾝﾄが知識ベースからの論理的推論を行うという問題は決定不能である」

実際に、エージェントが論理ベースから推論できることを決定できることが必要だろうか?
一般にはないだろう。エージェントは、多種類の推論エンジンを持っているかもしれず、また、接続手段、データ格納スペース、インデックスへのアクセス、処理パワーも様々であり、実際に推論できる能力もまちまちになる。Webの全体サイズに対して非決定的で多項式時間となるようなアルゴリズムは実用的ではないし、場合によっては線形時間であっても現実的ではない。Webのトポロジーや、あらかじめコンパイルされたインデックスのようなショートカットや処理しなくてよいリストの知識によりを知っているなどで、現実的には計算の複雑さは保証される。

一階述語論理より弱い言語にするのは、アプリケーションにとっては極めてリーズナブルである。ただ、Webにとってはあまり関係ない。

## Decidability
決定可能性

## 前世紀の論理学者は、どの文も真か偽のいずれかという言語を探すことが夢であった。そのため、例えば真か真でないかいずれにも分類できない自己矛盾した文の可能性を除くように言語を制限するという試みがあった。セマンティックWebでは、これはアカデミックな問題にすぎないように思える。というのは、実際扱うのは信頼できないデータの集まりだし、使えるのはWebの一部にすぎないからだ。

明らかに、自己矛盾の文は導びけないほうが良いが、言語がそのようなことを表現する十分な能力を持っていても良い。実際、署名システムは「この文は間違っている」ということが言えなければならないず、それにより、偶然的か必然的か、自己矛盾がおこる。自己矛盾を見つけたシステムの典型的なレスポンスは、その矛盾を見つけたので、例えば、同じソース(または、公開鍵)からの情報は信じないとするようなものかもしれない。

### Higher Order Logic
高階論理

### 「高階論理のための公理とルールの良いセットがない」ということは、常識を数学的に記述するのに困るだけでなく、電子商取引においてもある種のオペレーションは高階論理でないと自然に書けないため悩ましい。また、自分自身をルールで記述できることは、プログラム言語で自分自身のコンパイラが書けるのと同じように有用なことである。
フレーゲが二階論理に挑戦しようとしたとき、ラッセルは彼の論理の矛盾を指摘したと理解している。しかし、言語がコンシステントであり（公理から矛盾を導かない）、例えば以下のような性質を持つようにすることはできる。

現実的な方法で人間の信用をモデル化する。
XMLからRDF論理への対応を書き、定理はXML (論理をXML表現で書いたバイトストリーム)で証明することを許す。

そのようなルールは、RDF３つ組の推論を、その３つ組を代数的に導く意味コンテンツを持つメッセージとして書くようなものである。

forall message,t, r, x, y (
(signed(message,K)
& derivable(t, message)
& subject(t, x)
& predicate(t, r)
& object(t, y))
-> r(x,y)
)

(Kは特定の公開鍵であり、tは3つ組とする)

これにより言語の構造を扱う前提と、言語の内容に関連する結論との間の境界はなくなる。我々にはそういうことが必要なのか、または複数のマシンを用意し、1つのマシンで「信用できる」メッセージストリームを準備させてグラフに変換し、二番目のマシンは最初のとは知識空間を共有せずに推論して結果を出すのか?　これは絶望的に思える。というのも、実際にはバックエンド側の推論のためにフロントエンド側で新しい文書を検索したりすることはよくあるからである。しかし、これはすべて勘である。

Peregrinは[Peregrin]にて高階論理(HOL)のニーズと問題を分類しようとした。彼の高階論理のHenkinian解釈によると、述語はオブジェクト(individual)のサブクラスであると説明しており、現在の私のRDFとロジックのマッピングの理解に合う。つまり、RDF
predicateをRDFノードのサブクラスと考えるのである。確かにRDFでは、propertyタイプは、URIを述語として使うことで導くことが可能である:

forall p,x,y p(x,y) -> type(p, property)

そして、我々は、assert述語<rdf:property>は、その述語そのものと同じであると仮定する。

forall p,x,y assert(p,x,y) <--> p(x,y)

このように、２階論理の定式化と１階論理の定式化を移動することができる。

(2000) [PCA]による研究では、高階論理がこれらのシステムを統一する非常に現実的な方法であることを示すように思える。

## Yet to be addressed
(1999)

## 私は、個人的に高階論理で何が制限なのかを理解する必要がある…
そして、何が難しい制限であるか、そして、何が未解決なのか?

Fregeの二階論理(言うまでもなく常識の定式化)は、ラッセルが矛盾を引き起こすと発見したようにバグのあるものなのか、あるいは、常識の推論を行う数学的体系そのものが不可能なのか?そう、Fregeはどんな命題も真か偽のどちらかでないといけないという古典論理を使っていたようである。

演繹できないvalidな文があるという時に、"valid" という語で何を表しているのだろう。述語論理では、validityは真理値表、つまり全ての変数の真偽の組み合わせとして[Burris]定義することができる。この方法は、代数的にはいわば選言標準形にマップすることで推論するのと同じであり、言語の外部におけるオペレーションではない。
変数の値が制限されていないロジックには、この方法は実用的ではない。
このようにして、言語の外における常識のロジックへと戻ってしまう。

高階論理では、直観的には、その論理自体で正当性を証明することができなければならない。ゲーデルの不完全性定理では、明確にvalidity（正当性）とderivability（演繹可能性）の違いを記述しているので、おそらくその区別は必要となるだろう[DanC]。その答えがWebにあるかどうかは疑問である。

After a hallway chat with Peter SP-S, DMAL meeting 2001/2/14:

パラドックスの問題は、単にパラドックスを表現してしまうだけではない。パラドックスを含むロジックは、偽を推論してしまうのである。パラドックスの表現能力を与えるか、「pかnot
pのどちらか」という公理を与えるかのいずれかである。一階論理を元にこのようなことを行ったロジックの試みは2つのグループに分けられる。

集合を扱うことのできるロジックは多いが、集合を例えばwell-formedなものに制限することが多い。つまり、空集合か、その集合自体ではない少なくとも一つの要素を含むものか。このような制限を与えることで、ラッセルパラドックスの集合（自分自身に含まれない集合）は、well-formedでないとして避けることができる。ピーターが認めるように、ウェブにおいて、人々がパラドックスを表すのにこの方法をとるというのは馬鹿げている。

もう片方の方法は多くの信奉者がいる。その何人かは複雑すぎるとも言う。しかし、この方向にしか道は開けていないだろう。私が考えているセマンティックWebのアプリケーションの大半では、ルールや公理は全く完全ではないことに気づく。各アプリケーションは、それ自身の公理集合を持ち、それぞれコンシステントだったりそうでなかったりする。そのため、標準化に踏み出す方向としては、セマンティックWebにおける各文書やメッセージに、それが使う語彙、論理結合子、利用する公理へのポインターを付与することである。

@@@

Mapping RDB and SM models - defining URIs;
;
nulls;
etc.
References

[PCA] Proof-Carrying Authentication. Andrew W. Appel and
Edward W. Felten, 6th ACM Conference on Computer and Communications Security,
November 1999. (background) Mar 2000 discovery. based on [LF]

[Burris] Stanley N. Burris, Logic for Mathematics and
Computer Science, Prentice Hall 1998.

[BurrisSup]Supplementary text to the above.

[Cheng] The ERM model paper, available in [Laplante]

[ConnollySoLREK] Dan Connolly's home page for this sort
of stuff. "A Study of Linguistics: Representation and Exchange of Knowledge".

[Crawf90]

ALL: Formalizing Access Limited Reasoning
J. M. Crawford jc@cs.utexas.edu
Benjamin Kuipers kuipers@cs.utexas.edu
Department of Computer Sciences
The University of Texas At Austin
Austin, Texas 78712
25 May 1990
Abstract

Access-Limited Logic (ALL) は、ネットワーク状知識ベースでアクセスできる範囲が制限されている場合の知識表現言語である。古典論理や、論理プログラム言語では、与えられたパターンにマッチする全ての言明を対象とするのに対して、ALLでは有効なアクセスパスで到達できる言明のみを扱うことができる。推論の複雑さは知識べ―ス全体の大きさとは無関係で、近隣のネットワーク結節度に依存する。ALLは不完全であるものの、セマンティックスはwell
definedであり、完全性も弱い形で保証する。Socratic Completeness、つまり知識ベースの論理的帰結であるどのような質問に対しても、それに続く一連の質問がある。ここでは、ALLの概要と、Socratic
Completenessのスケッチと証明、多項式オーダーの計算コストについて述べている。

algernon papers

[Crawf91] J. M. Crawford and B.J. Kuipers, "Negation and
proof by Contradiction in Access Limited Logic", in Proceedings of the
Ninth National Conference on Artificial Intelligence (AAA1-91), Cambridge
MA, 1991

[Date] An Introduction to Database Systems, 6th Edn, Adison-Wesley,
1995

[Davis] Randall Davis and Howard Schrobe, "6.871: Knowledge
Based Application Systems" course supporting information, 1999

[HOLintro]M. J. C. Gordon and T. F. Melham, "Introduction
to HOL A theorem proving environment for higher order logic", Cambridge
University Press, 1993 ISBN 0 521 44189 7

[Laplante] Phillip Laplante (Ed.), "Great Papers in Computer
Science", West, 1996, ISBN:0-314-06365-X

[Marchiori98] M. Marchiori, Metalog paper at QL98

[Peregrin] Jaroslav Peregrin, "What Does One Need, When
She Needs "Higher-Order Logic?" Proceedings of LOGICA'96, FILOSOFIA, Praha,
1997, 75-92

[VLFM] J. P. Bowen, Formal Methods, in WWW Virtual Library

@@

Much of this is following in the wake of Dan
Connolly's investigations, and so many of the references were provided
directly or indictly by Dan.Other pointers from Dan Connolly

DC on the need for HOL - private communication

[LF] Harper, Honsell, Plotkin "A Framework for Defining Logics",
Journal of the ACM, January 1993 appears to be the seminal paper on ELF
paper (ACM pdf)
connolly's (attempted) transcription into larch

Pat Hayes mentioned a logic in which the law of the excluded
middle does not exist - which si important as you can always considera
paradox which is neither true nor false. See email 2000/09/01

より適した基本となるロジックは一般的なホーン節論理だろう。これは、論理プログラムで使われた一階述語論理のホーン節によるサブセットのようなものである。full
negation (計算コストがかかる）や、NAF (失敗としての否定; 計算コストは安いが、非単調的）の変わりに、intuitionistic
(constructive) negationを利用している。intuitionistic negationとは、full
negationに似ているが、矛盾による証明は除外している。有名なホームズが言うように、不可能を除いていくというようなことには使えない）。これは、計算可能であり、単調であり、きちんとしたセマンティックスがある。これは、ホーン節論理の多くの利点をそのままに、制限を除いたものである。実装も行われて、いくつかのアプリケーションにも使われている。詳しくは以下を参照のこと。
http://citeseer.nj.nec.com/hogan98putting.htmlhttp://citeseer.nj.nec.com/hogan98putting.html,
especially the 1996 "meta-programming...." and the main citation at the
top. For the raw logic follow the McCarty 88 references.

quoted without permission. DanC recommends Non-Contradiction
and Excluded Middle in Peter Suber's Logical Systems course notes as an
explanation of intuitionistic logic. TimBL noted the same bit that I did
on first reading:

In the world of metamathematics, the intuitionists
are not at all exotic, despite the centrality of the PEDC (hence the PEM)
to the ordinary sense of consistency. Their opponents do not scorn them
as irrationalists but, if anything, pity them for the scruples that do
not permit them to enjoy some "perfectly good" mathematics.

Pat Hayes, Research Interests and Selected Papers
contains stuff on time modelsImpl

Reiter, R., On Closed World Data Bases, in: H. Gallaire
and J Minker (eds.), Logic and Data Bases, Plenum, 1978, pp. 55-76. Defines
Cloased World Assumption? Ref from CIL

## Footnotes

## "Second-order logic is rather difficult to study, since it
lacks a decent set of axioms and rules of inference, so we have little
to say about it" -- Footnote to preface to [Burris], p.xii