Resolution Principleとは

Resolution Principleとは、前提として書いた論理の文(述語論理の文)から、ある結論が必ず導けるかどうかを、コンピュータに確かめさせるための規則です。日本語では導出原理と呼ばれます。米アルゴンヌ国立研究所とライス大学に属していたJ・A・ロビンソン氏が、1965年1月に米国計算機学会(ACM)の論文誌で発表しました。使う規則がこれ1つだけでも、矛盾を含む前提なら、いつか必ずその矛盾を見つけ出せるのが特徴です。

どうやって、結論が正しいと確かめるの？

ロビンソン氏の方式は、結論を正面から証明しにいきません。結論を打ち消した文を前提に加え、全体が矛盾していることを示す、という進め方です。矛盾が出れば、元の結論は前提から必ず導けたことになります。数学の背理法に近い考え方で、論文に載っている代数の問題でも、示したい結論(ある性質を持つ要素が存在する)を「存在しない」と打ち消して前提に加え、そこから矛盾を導いています。

矛盾を探すときに使う規則が、導出原理です。中身は、「AまたはB」と「Aではない」という2つの文があれば、Aを打ち消し合わせて「B」を残す、というもの。たとえば「在庫がある、または取り寄せになる」と「在庫はない」からは、「取り寄せになる」が残ります。これを繰り返して、最後に中身が何も残らない文(空の文)が出てきたら、前提どうしがぶつかっている、つまり矛盾がある、という判定です。

「すべての取引先について〜」のように、変数を含む文どうしを組み合わせるときは、変数に何を当てはめれば2つの式がそろうかを、探さなければなりません。ロビンソン氏は同じ論文で、その当てはめ方のうち最も一般的なものを機械的に求める手順(単一化)も示しました。

なぜ「機械向け」の論理なのか

論文の題名は「A Machine-Oriented Logic Based on the Resolution Principle(導出原理にもとづく、機械向けの論理)」。序論によると、それまでの論理学では、証明の1歩1歩は、人が一度見ただけで正しいと納得できるくらい単純でなければならない、とされてきました。ロビンソン氏は、規則を当てはめるのがコンピュータなら、この制限はもう適切ではないと考え、人には1歩では見通せないほど大きな1歩を、正しく踏める規則を選んだ、と書いています。論文の言い方を借りれば、「人間向けではなく、機械向け」。

論文自身は、規則1つで矛盾を必ず見つけられることを「それほど重要ではない」とし、一番の利点は、それまでの方式の計算量の壁を避けられる点だと述べています。論文の最初の例では、以前の方式で同じ答えにたどり着こうとすると、確かめる文の数が10の256乗ほどに膨らみ、とても実行できません。導出原理なら、1回の組み合わせで矛盾が出ます。別の例では、ギルモア氏がIBM 704で動かした以前のプログラムが21分たっても答えを出せず、デイビス氏とパトナム氏の効率のよい方式でも手計算で30分かかった問題を、導出原理と簡略化の決まりを使って6段階の書き換えで2つの文に絞り、すぐに矛盾を出しています。

どんな問題でも、必ず答えが出る？

いいえ。前提に矛盾があれば、いつか必ず見つかります。困るのは矛盾がないときで、計算がいつまでも終わらないことがあるのです。論文も、チャーチの定理を引いて、どんな正しい手順でも入力によっては止まらずに計算を続けてしまう、と認めました。例として載っているのは、自然数の性質を書いた2つの文から、新しい文がいつまでも生まれ続けるケース。「矛盾がない」と言い切れるかどうかは、問題しだいということです。

導出原理は、その後どう使われた？

ロジック・プログラミングの草創期を当事者として振り返ったロバート・コワルスキー氏は、1988年の回想で、最も素直な形のロジック・プログラミングとは、知識を「〜ならば〜」という形の文(ホーン節)で書き、答えたい問いから前提の側へ逆にたどる演繹を、導出原理に組み込んで計算することだ、と書いています。その代表がPrologです。1972年の夏に、仏マルセイユのアラン・コルメロエ氏とフィリップ・ルーセル氏が開発しました。

ただし、評価はまっすぐ上がったわけではありません。同じ回想によると、1970年代の初めには、北米のAI研究者の多くにとって、導出原理はとうに評価を落としたものになっていました。流行は、どんな問題にも使える定理証明から、知識を手続きとして書く方式(その代表がPlanner)へ移り、導出原理を使い続けた英エディンバラ大学の研究者たちは、しだいに孤立していった、とコワルスキー氏は振り返っています。

Resolution Principleに関するよくある質問

導出原理と述語論理は、何が違うのですか？

述語論理は、「すべての〜は」「ある〜が存在する」といった言い方も含めて、知識を厳密に書くための言葉の体系です。導出原理は、その言葉で書いた文どうしを組み合わせて、新しい文を導くための規則です。1965年の論文は、1階の述語論理を、規則が導出原理1つだけになるように組み立て直しました。作者の知る限り、規則1つだけで完全な体系はそれまでなかった、と論文は書いています。

論文の手順は、そのままで実用になったのですか？

論文自身が、手順をそのまま実装すると非常に効率が悪い、と書いています。そのうえで最後の節で、無駄を減らす決まりを3つ示しました。どの文とも打ち消し合えない部分を含む文を外す決まり(purity)、もっと一般的な文に含まれてしまう文を外す決まり(subsumption)、新しく導いた文が元の文を含むときに置き換える決まり(replacement)です。より詳しい扱いは、続く論文で行う予定だとしています。