20世紀の名著名論

J. A. Robinson: A Machine-Oriented Logic Based on the Resolution Principle

Journal of the ACM, Vol.12, No.1 (1965), pp.23-41.


 これは,自動定理証明の研究にブレークスルーを与えるとともに,1970年代以降に発展をとげた論理プログラミングパラダイムの礎ともなった論文である.

 哲学の学位をもつ著者 Alan Robinson(1930〜)は,学問においても学問以外においても大変に懐が深い英国紳士である.ピアノの名手でもあり,Robinson(ピアノ),Jacques Cohen(ブランダイス大学,バイオリン),古川康一(慶應義塾大学,チェロ)によるピアノ三重奏は,論理プログラミング国際会議の恒例社交行事となっていた.私もご縁があって,演奏会のピアノ譜めくりをつとめたことがある.

 さて論文タイトルの resolution principle(融合原理)は,一階述語論理のための単純で強力な演繹の手法である.話を簡単にするために一階述語論理のサブセットである命題論理に限定すると,たとえば Por (not Q) or R という(or でつながった形式の)論理式と (not R) or S or U という論理式の中から,R と (not R) という,形は同じで極性(not の有無)の異なるペアをみつけてキャンセルし,残りをつなぎあわせて P or (not Q) or S or U という論理式を導くのが融合である.P implies Q が (not P) or Q とも書けることに注意すれば,融合は,P と P impliesQ から Q を導く三段論法や,P と (not P) から“偽”(= or 演算の単位元)つまり矛盾を導く作業を特別な場合として含むことがわかる.

 一階述語論理の場合は,上記の P, Q, ... の部分が原子論理式(述語に引数を与えたもの)となる.たとえば (not Human(x)) or Mortal(x) という論理式は,先頭に ∀x がついたもの(すべての人間は死を免れない)と見なすが,これと Human(Socrates) とを融合しようとする場合,まず x に Socrates を入れて (not Human(Socrates)) or Mortal(Socrates) を作る.しかるのちに命題論理の場合と同様にMortal(Socrates) を導く.このように,変数の値を具体化して複数の原子論理式の形を同じにする作業をunification(単一化)という.

 Resolution は,導出,分解,融合などいくつもの訳語を産んだ.分解と融合に至ってはほとんど反意語にしか見えないが,よりすっきりした形にもってゆくというのが resolution の本来の意味である.

 一階述語論理の定理証明における最も基本的な結果として,23歳にして山岳遭難で死亡した Herbrand の定理がある.これは述語論理における証明を本質的に命題論理レベルの証明に還元する方法を与えるものだが,Robinson は,この還元作業を“的を射た”効率的なものにしようとして融合原理にたどりついた.アルゴンヌ国立研究所(ANL)在職中の仕事である.ANL は,昔も今も自動定理証明研究の世界的拠点で,ANL で開発されたシステム EQP が代数学における Robbins の予想(1933)を1996年に肯定的に解決したことは,この分野の近年の大きな成果として知られる.

 標題の中の“Machine-Oriented”は,自然演繹法のような“人間向き”の論理体系との対照を意図したものだが,人工知能論の試験答案を毎年採点してみると,融合原理を用いた証明問題は一貫して正答率が高い.その意味ではとても人間に優しい方法だとも言える.

 本論文のもう一つの大きな貢献は,単一化という概念をはじめてきちんと定式化し,アルゴリズムを与えて証明したことである.単一化は,定理証明や論理プログラミングだけでなく,プログラムの型解析や自然言語文法など広範な分野で活用されている.日本の大学教科書シリーズとしては異例のボリュームを誇る岩波講座ソフトウェア科学では,全17冊のうちの少なくとも8冊に単一化がとりあげられている.

 JACM の論文は難しいというのが大方の印象であろうが,本論文は,学部生にも読むことのできる古典として勧められる.ACM のデジタル図書館から PDF が入手できるが,今年のゼミで本論文を担当した学部4年の圷弘明君が,p.34にスキャンミスによる欠落があることを発見した.すぐに,東大武市研からいただいた青焼コピー用第2原図が手許にあることに気がつき,湿式複写機時代の古文書が21世紀に有効に活用された.

上田和紀/早稲田大学 理工学部 情報学科
(情報処理,Vol.43, No.7(2002年7月号), p.792 所収)


Kazunori UEDA
Last modified: Sun Jan 5 00:13:23 JST 2003