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自体は推論エンジンを規定しない。それは、有効なオペレーションを定義し、それらが一貫していることが必要となる。一般に、セマンティックWebでは、定理の証明をフォローできればよく、証明を作り出す必要はない。

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

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

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

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

• セマンティック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
複雑性と決定不能性

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

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

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

Decidability
決定可能性

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

Higher Order Logic
高階論理

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

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

これにより言語の構造を扱う前提と、言語の内容に関連する結論との間の境界はなくなる。我々にはそういうことが必要なのか、または複数のマシンを用意し、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

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