2005 年 10 月 7 日 伊藤先生演習用資料作成

久木田

2.3 節までのまとめ
以下，簡単に Gillies 氏のテキストを振り返ります．

¶ 帰納主義と反証主義：科学的方法については対立する二つの理論がある．一つはベーコンに代表される帰納主義であり，もう一つはポッパーに代表される反証主義である．前者が与えられたデータからの機械的な推論による一般法則の導出という方法を重んじるのに対して，後者は科学者のひらめきによる仮説の形成とデータによる反証という方法を重んじる．科学史の事例を見ると，ベーコンが考えたような純粋に機械的な推論によって重要な発見がなされている例はなさそうに思われる．しかしながら機械学習と呼ばれる AI の分野の近年の発展はこの状況を変化させてきている．

¶ 機械学習：機械学習は「チューリング的伝統」の中で発展してきた AI の一分野である．これは，決まったアルゴリズムにしたがってデータと背景知識から一般化を導出するものであり，ベー
コン的帰納法と適切に呼ばれうるものであるかもしれない．

¶ チューリング的伝統：チューリング的伝統は，(1) 論理の使用と，(2) 実際的問題への応用の重視によって特徴付けられる．機械学習にとって (1) が重要であるのは，論理主義の提唱者のフレーゲが考えたように，推論のステップを厳密に隙間なく構成することによって，推論のメカニズム
をシミュレートできるからである．これを行わずに単に人間の帰納的推論をなぞるだけでは，人間がすでに発見したことを再発見することは出来るかもしれないが，新しい事実の発見には繋がらない．

¶ エキスパート・システムと Feigenbaum’s bottleneck：チューリング的伝統の実用的側面は，エ
キスパート・システムに現れる．これは人間のエキスパートによって行われていた推論・判断を
機械によって行わせる試みである．このようなシステムを作る際には，まず人間のエキスパート
がどのようにして彼らの仕事を行っているかを明確なルールとして定式化しなければいけないが，これは手間がかかる上に，エキスパート自身がそのようなルールをはっきりとは意識しておらず，
うまく説明できないことが多い．これが Feigenbaum’s bottleneck といわれる問題である．ところがこのようなルールを明示化するのに機械学習が有用であることが分かってきた．

¶

ID3：Quilan によって開発された ID3 は，対象の集合と属性の集合が与えられたときに，その対象の集合をある分類に関してポジティブな事例とネガティヴな事例に完全に分けるような属性の束を見つけるよう設計された機械学習システムである．ID3 の顕著な特徴は general-to-specific
的，トップ・ダウン的な性格を持っているということである．ID3 は与えられた対象の集合に対して何らかの属性による分割を試みる．こうして新しく作られた部分集合に対して再び別な属性を1

適用し，さらに分割をすすめる．この過程を続けて，最終的にすべての部分集合がポジティブな事例かネガティブな事例のどちらかしか含まないようであれば，そのような分類を可能にした属
性の束が最初に与えられた分類を特徴付ける性質であると考えることができる1 ．

ID3 の短所は属性ベースで設計されているためにデータとして一項述語しか使えないことである．ID3 でも十分に役に立つ場合もあるが，しかし一階述語論理の資源，つまり多項関係を使いたい場合もある．そこで一階述語論理に基づいたシステムが開発されている．

大体以上が前期にやった話でした．Gillies 氏のテキストはこの先，関係ベースの機械学習システ
ム GOLEM の説明にはいります．GOLEM はエキスパート・システムに必要な規則を生み出すだ
けでなく，与えられたデータと背景知識から，決まったアルゴリズムとヒューリスティックによって新しい自然法則を発見することができること，それゆえベーコンの考えた機械的な帰納法のモデルになりうるものであることが論じられます．

GOLEM は Robinson のレゾルーション原理を基にした規則を使っているということですが，そこのところがあまり詳しく説明されていないので，そもそものレゾルーション原理がどういうものであり，それが機械学習にどのように応用されているのかを以下で簡単にリポートします．

1

レゾルーション原理

1.1

前置き

AI 研究において，論理学と AI の関係，あるいは前者が後者に対して持つ意義は，一つの大きなテーマである．AI が人間の知性のモデルであると考えられるならば，この問題は，論理学が人間の思考にとってどういう意義を持っているのか，というより大きな問題にかかわってくる．現
実の状況における判断と行動という側面を考えた場合，論理的思考というものの重要性・意義については疑問が持たれてきた．例えば「フレーム問題」に関する議論がある．行為者が何らかの目的をもって行動するとき，彼は無限の情報を含む環境の中で，自らの目的にとって関連性の高い情報をとりだし，そこに基づいて推論・判断し，そして行為しなければならない．この様な場
合，論理学というものはほとんど役に立たないと考えられている．人間の思考や行動における環境との相互作用が重視されてくるにつれて，人間的思考のモデルとしての論理学という考え方は，
ますます旗色が悪くなっている．人間は与えられたデータと背景知識から仮説を立て，その仮説から予測を引き出し，その予測に基づいて行動する．この過程は必ずしも論理的・演繹的なものではない．
しかしその一方で，論理プログラミングに基づいた機械学習システムが近年大きな成功を収めてきている．これらのシステムの中には決められたアルゴリズムに従いながら帰納的推論

1

正確に言えばこの属性の束は，個々の属性を原子式として捉えた場合，選言標準形で表されるであろう．

2

与えられた例からの一般化を行うものがある．例えば Quinlan の ID3 がそのようなシステムの一つである．ID3 の短所はそれが一項述語しか利用できないため，応用の範囲が限られているということであった．そこで Quinlan は関係をベースにした学習システム FOIL を開発した．FOIL
も ID3 と同様にトップ・ダウン的性格を持っている．またエントロピーに関連付けられた情報利
得 information gain の規準に基づいている点も ID3 と同様である．

FOIL のようなシステムに対して Plotkin，Muggleton らはやはり関係をベースにしながら，
specific-to-general 的，ボトム・アップ的な性格を持った機械学習システムを開発した．彼らのシステムはレゾルーション原理 the resolution principle（以下 RP）という原理を利用している．これはそもそもは J. A. Robinson によって提案された論理体系の推論規則として採用されていたものである．Robinson 自身はこの体系を，コンピューターによる定理証明プログラムの理論的な枠組みとして構築したのであるが，Muggleton らは RP による新しい命題の導出過程を逆転させることによって，与えられたデータから新しい述語を生成させるプログラムを作り上げた．また RP 以
外にも，Robinson のシステムで使われた置換 subustitution，統合 unification，包摂 subsumptionなどの概念は Plotkin，Muggleton らのシステムにおいて重要な役割を果たしている．

RP の基本的なアイディアは次のようなものである．ある命題（正確には RP は命題ではなく，リテラル literals と呼ばれる命題の集合（この集合はクローズ clauses と呼ばれる）の集合を適用の対象とする）に RP を繰り返し適用することによって，もし元の命題が矛盾を含むものであれば，その矛盾を明白にするというものである．通常の論理学の体系が，公理から推論規則によって定理を導出していくのに対して，Robinson の体系は，任意の命題についてその反証を探すこと
で，もとの命題が定理であるかどうかを確かめる，という方法を採用している．もちろんこれは
いわゆる分析的反証法の一種だが，Robinson の方法の利点は，それが RP のみを適用することから成り立っているということである．RP は通常の述語論理の公理系や証明論における推論規則と比べると非常に複雑であるが，Robinson の論文のタイトルにもあるように，RP は基本的にコンピューターに実行させるように作られた規則であり，その上では利点がある．
以下，Robinson (1965) に基づいて RP の概略を述べる．

1.2

シンタクス

この体系は通常の 1 階述語論理とは異なり，妥当性と証明の概念ではなく，充足不可能性と反証の概念に基づいて立てられている．1 階論理の文の有限集合 S が充足可能であるかどうかを決定するには，それぞれの文は存在量化子を持たない冠頭標準形2 であると想定すれば十分である．な
おかつそれぞれの文のマトリクス3 は，原子式4 もしくは原子式の否定を選言肢として持つ選言であると想定しても良い．
2

量化子が文の頭についている形．

3

冠頭標準形の文から量化子を取り除いた残り．

4

論理結合子を含まない論理式．

3

そこでこの体系は文法的な単位としてこの特殊な形式の文の有限集合を持つ．冠頭量化子は省略される．というのもそれはすべての自由変項に対する全称量化子であると決まっているからだ．さらには選言記号も使われない．問題としている集合がリテラル（後述）が複数含んでいるならば，その選言が私たちが考慮している命題であるとわかるからである．例えば集合 S が A(x), ¬B(y, x)を含んでいたら，この集合は ∀x∀y(A(x) ∨ ¬B(y, x)) という命題を表している．
定義 1.1 (変項). 以下の記号が変項である．アルファベット的順序で並べてある：

u, v, w, x, y, z, u1 , v1 , w1 , x1 , y1 , z1 , u2 , . . . , etc.
定義 1.2 (関数記号). 0 以上の n それぞれについて，以下の記号が n 度の関数記号である．アルファベット的順序で並べてある：

an , bn , cn , dn , en , f n , g n , hn , k n , an1 , bn1 , . . . , etc.
n = 0 の場合は上添字は省略しても良い．0 度の関数記号は個体定項である．
定義 1.3 (述語記号). 0 以上の n それぞれについて，以下の記号が n 度の述語記号である．アルファベット的順序で並べてある：

P n , Qn , Rn , P1n , Qn1 , R1n , P2n , . . . , etc.
n = 0 のとき上添字は省略しても良い．
定義 1.4 (否定記号). ¬.
定義 1.5 (記号のアルファベット的順序). すべての記号の集合はアルファベット的順序によって整列される5 ．これは上の並べ方の規約に以下の規則を付け加えることで定義される．変項は関数記号に先行する．関数記号は述語記号に先行する．述語記号は否定記号に先行する．度数のより低い関数記号は度数のより高い関数記号に先行する．度数のより低い述語記号は度数のより高い述語記号に先行する．
定義 1.6 (項). 変項は項である．n 度の関数記号とその後ろについた n 個の項からなる記号の列は項である（ただし n ≥ 0）．
定義 1.7 (原子式). n 度の述語記号とその後ろについた n 個の項からなる記号の列は原子式である（ただし n ≥ 0）．
定義 1.8 (リテラルLiterals). 原子式はリテラルである．A が原子式ならば，¬A はリテラルである．前者を正のリテラル，後者を負のリテラルということもある．
ある集合 S の元の間に順序関係 ⪯ が定義されており，S の任意の二つの元 a, b に関して a ⪯ b か b ⪯ a のどちらかが成り立ち，また S の任意の部分集合において，⪯ に関する最小元が存在するとき，S は ⪯ によって整列されると
いう．
5

4

定義 1.9 (補式). A が原子式ならば，A と ¬A という二つのリテラルは互いの補式であるといい，またこの二つは，どちらの順序でも，相補的対を形成するという．L がリテラルであるとき，L に
よって L の補式を表す場合がある．
定義 1.10 (クローズClauses). リテラルの有限集合（空でも良い）．空のクローズは □ によって指示される．
定義 1.11 (ホーン・クローズ Horn clauses). 正のリテラルを一つだけ持つクローズ．ホーン・
クローズだけからなる集合を論理プログラムという場合がある6 ．
定義 1.12 (基礎リテラル). 変項を含まないリテラル．
定義 1.13 (基礎クローズ). 基礎リテラル以外を含まないクローズ．命題クローズという場合もある．□ も基礎クローズである．
定義 1.14 (適格な表現Well-formed expressions). 項とリテラルは適格な表現である（以下「WFE」）．それ以外に WFE はない．見やすさのために，関数記号と述語記号の後ろにくる項を() でくくり，もし項が複数あるなら間をコンマで区切ることにする．このとき上添字を省略することができる．例えば P 2 yh3 bvf 1 x と書く代わりに P (y, h(b, v, f (x))) と書く．
定義 1.15 (WFE の辞書的順序). すべての WFE は辞書的順序に整列される．この順序は次の規則によって決定される．A が B に先行するのは，A が B よりも短いか，もしくは同じ長さで，Aと B が異なる記号を持つ最初の位置で，A が B よりもアルファベット的順序で先行する記号を持つ場合である．

1.3

充足可能性と基礎レゾルーション，いくつかの定理

定義 1.16 (エルブラン宇宙Herbrand universes). 任意のクローズの集合 S に対して，S のエルブラン宇宙 HS と呼ばれる，基礎項からなる次のような集合が結び付けられる．まず F は S に現れるすべての関数記号の集合であるとする．F が 0 度の関数記号を含んでいるなら，S の関数
語彙は F である．もし含んでいなければ，S の関数語彙は {a} ∪ F である．このとき HS は，Sの関数語彙のみから構成されるすべての基礎項の集合である．例えば S の関数語彙が {a, f 1 , g 1 }ならば HS は {a, f (a), g(a), f (f (a)), f (g(a)), g(f (a)), g(g(a)), ...} である．
定義 1.17 (充満Saturation). S は任意のクローズの集合，P は任意の項の集合とする．このとき P (S) によって，P 上での S の充満を表す．これは S の要素に現れる変項を P の要素によって置き換えて得られるすべての基礎クローズの集合である．ただし同じ変項の現れはすべて同じ項で置き換えられるものとする．
6

13 頁，例 2.7 参照

5定義 1.18 (モデル). 相補的な対をふくまない基礎リテラルの集合．M がモデル，S が基礎クローズの集合であるとする．S に属するすべての C が M の要素を含んでいるとき，M は S のモデルであるという．
定義 1.19 (充足可能性). クローズの集合 S にモデルが存在するとき，S は充足可能である．そうでないとき，S は充足不可能である．
定義から明らかなように，□ を含むクローズの集合は充足不可能である．また空集合は充足可能である．空でないクローズはそこに含まれるリテラルを選言肢とする選言に対して全称量化を施した閉式として解釈される．
定義 1.20 (基礎リゾルヴェント). C と D が基礎クローズであり，L ⊆ C, M ⊆ D はともにシング
ルトン（単元集合）であり，その要素が相補的対を形成するとき，基礎クローズ (C − L) ∪ (D − M )は C と D の基礎リゾルヴェントと呼ばれる．

R が C と D の基礎リゾルヴェントであるとき，明らかに {C, D} の任意のモデルは {C, D, R}のモデルでもある．任意の基礎クローズの対は高々有限の基礎リゾルヴェントしか持たない（クローズは有限集合であることに注意）．
定義 1.21 (基礎レゾルーション). S は基礎クローズからなる任意の集合であるとする．このときS の基礎レゾルーション R(S) は，S の要素になっているすべての基礎クローズと，S の任意の二つの要素のすべての基礎リゾルヴェントからなる集合である．
定義 1.22 (n 次基礎レゾルーション). S は基礎クローズからなる任意の集合であるとする．このとき S の n 次基礎レゾルーション R n (S) は以下のように定義される．R 0 (S) = S; 任意の n ≥ 0に対して，R n+1 (S) = R(R n (S))．
定理 1.23 (Herbrand’s Theorem). S はクローズからなる任意の有限集合であり，HS はそのエルブラン宇宙であるとする．このとき，S が充足不可能なのは，HS (S) のある有限な部分集合が充足不可能なときであり，そしてそのときに限る．
この定理は次のようにも表現できる．
定理 1.24. S はクローズからなる任意の有限集合であるとすると，S が充足不可能なのは，HSのある有限な部分集合 P に対して，P (S) が充足不可能なときである．
さらに S が充足不可能であり，その反証が存在するならば，定理の条件を満たす最小限の P を構成することができる．そのような P は S についての proof set と呼ばれる．
定理 1.25 (Ground Resolution Theorem). S が基礎クローズからなる任意の有限集合である
とき，S が充足不可能であるのは，ある n ≥ 0 に対して，R n (S) が □ を含むときであり，そしてそのときに限る．

6

定理 1.26. S がクローズからなる任意の有限集合であるとき，S が充足不可能であるのは，HSのある有限な部分集合 P とある n ≥ 0 に対して，R n (P (S)) が □ を含むときであり，そしてそのときに限る．
補題 1.27. S がクローズからなる任意の集合であり，P が HS の任意の部分集合であるとき，

R(P (S)) ⊆ P (R(S))．
系 1.28. S がクローズからなる任意の集合であり，P が HS の任意の部分集合であるとき，すべての n ≥ 0 に対して，R n (P (S)) ⊆ P (R n (S))．
定理 1.29. S がクローズからなる任意の有限集合であるとき，S が充足不可能であるのは，HSのある有限の部分集合 P とある n ≥ 0 に対して，P (R n (S)) が □ を含むときであり，そしてそのときに限る．

1.4

置換，統合，レゾルーション，いくつかの定理

定義 1.30 (置換要素). V が任意の変項であり，T は V と異なる任意の項であるとき，T /V を置
換要素という．V を要素 V /T の変項といい，T を要素 V /T の項という．
定義 1.31 (置換). 置換要素の任意の有限集合（空である場合も許す）で，各要素の変項がどれも異なっているとき，この集合を置換という．P が項からなる任意の集合で，置換 θ の要素の項がすべて P に属するとき，θ は P 上の置換であるという．要素として T1 /V1 , . . . , Tk /Vk を持つ置換
を {T1 /V1 , . . . , Tk /Vk } と書く．このとき要素の順序はどうでもよい．ギリシャ文字の小文字を置換を表すために用いる．特に ϵ は空置換を表す．
定義 1.32 (例化). E は任意の有限の記号列であり，θ = {T1 /V1 , . . . , Tk /Vk } は任意の置換であるとする．このとき θ による E の例化とは，E における変項 Vi（1 ≤ i ≤ k ）の各現れを，項 Ti の現れによって置き換える操作である．その結果として得られる記号列を E の θ による例と呼び，Eθ
によって表す．C が記号列の任意の集合であり，θ が置換であるとすると，C の θ による例とは，{Eθ|E ∈ C} である．
定義 1.33 (標準化). C は記号列の有限集合であり，V1 , . . . , Vk は C に現れるすべての異なる変項をアルファベット的順序で並べたものである．このとき，C の x-標準化は，置換 {x1 /V1 , . . . , xk /Vk }であり，ξC と表す．また C の y-標準化は置換 {y1 /V1 , . . . , yk /Vk } であり，ηC と表す．
定義 1.34 (置換の合成). θ = {T1 /V1 , . . . , Tk /Vk } と λ は任意の二つの置換であるとする．λ′ は λの要素のうち，その変項が V1 , . . . , Vk のどれとも異なっているものの集合であるとする．また θ′は，Ti λ が Vi とは異なっているような要素 Ti λ/Vi（1 ≤ i ≤ k ）すべてからなる集合であるとする．
このとき θ′ ∪ λ′ を θ と λ の合成といい，θλ によって表す．

7

事実 1.35. 置換の合成は結合性を持つ．つまり任意の置換 σ, θ, λ について (σθ)λ = σ(θλ) が成り立つ．また E が任意の表現であり，θ, λ が任意の置換であるとすると，(Eθ)λ = E(θλ) が成り立つ．したがってこれらの括弧を省略しても構わない．
事実 1.36. θ，λ を任意の置換とする．すべての表現 E について，Eθ = Eλ ならば θ = λ が成り立つ．
事実 1.37. 任意の記号列の集合 A，B と置換 λ について，(A ∪ B)λ = Aλ ∪ Bλ が成り立つ．
定義 1.38 (不一致集合Disagreement sets). A は WFE の任意の集合であるとする．A に属す
る WFE の部分 WFE で，A に属する WFE のすべてが同じ記号を共有しているのではない，最初の場所に現れるものすべての集合を A の不一致集合という．
例 1.39.

A = {P (x, h(x, y), y), P (x, k(y), y), P (x, a, b)}
A の不一致集合 = {h(x, y), k(y), a}
定義 1.40 (統合Unification). A が WFE の任意の集合であり，θ が置換であるとする．Aθ がシングルトンであるとき，θ は A を統合する，あるいは θ は A の統合子であるといわれる．統合子を持つ WFE の任意の集合は，統合可能であるという．
明らかに，θ が A を統合するが A がシングルトンではないのであれば，θ は A の不一致集合を統合する．
定義 1.41 (統合アルゴリズム). WFE からなる任意の有限かつ空でない集合 A に対して適用される以下の手続きを，統合アルゴリズムという．
手順 1．σ0 = ϵ, k = 0 とし，手順 2 へ進め．
手順 2．Aσk がシングルトンでないならば手順 3 に進め．そうでなければ σA = σk として停止せよ．
手順 3．Aσk の不一致集合 Bk の要素を辞書的順序で並べたときに，最初に来るものを Vkとし，二番目に来るものを Uk とせよ．Vk が変項であり Uk の中に現れないのであれば，

σk+1 = σk {Uk /Vk } とし，k に 1 加えて，手順 2 に戻れ．そうでなければ停止せよ．
定義 1.42 (最汎統合子Most general unifiers). A は WFE の有限かつ空でない任意の集合．Aの統合アルゴリズムが手順 2 で停止するとき，その結果として得られる置換 σA は，A の最汎統合子という．またこのとき A は最汎統合可能であるという．
定義 1.43 (キー・トリプルKey triples). リテラルの有限集合 L, M, N の順序付けられた三つ組⟨L, M, N ⟩ は，以下の条件を満たすとき，クローズ C, D の順序付けられた対 ⟨C, D⟩ のキー・トリ
プルという．

8

(i)L と M は空ではなく，L ⊆ C, M ⊆ D．

(ii)

N は，集合 LξC ∪ M ηD の要素である原子式か，要素の補式である原子式からなる集合．

(iii)

N は最汎統合子 σN によって最汎統合可能である．

(iv)

集合 LξC σN と集合 M ηD σN はシングルトンであり，その要素は互いに補式である．

定義 1.44 (リゾルヴェント). C と D がクローズであり，⟨L, M, N ⟩ が ⟨C, D⟩ のキー・トリプルであるとき，クローズ (C − L)ξC σN ∪ (D − M )ηD σN ) を，C と D のリゾルヴェントと呼ぶ．
注意 1.45. 明らかに対 ⟨C, D⟩ は高々有限個のキー・トリプルを持つ．したがって C ，D は高々有限個のリゾルヴェントを持つ．
定義 1.46 (レゾルーション). S はクローズからなる任意の集合であるとする．このとき S のレゾ
ルーション R(S) は，S の要素と，S の要素のリゾルヴェントすべてからなる集合である．
定義 1.47 (n 次レゾルーション). S はクローズからなる任意の集合とする．S の n 次レゾルー
ション R n (S) は，n 次基礎レゾルーションとまったく同様に定義される．
注意 1.48. 前注意から分かるように，クローズからなる任意の集合 S に関してある n ≥ 0 が存在
し，m ≥ n なる任意の m について R n (S) = R m (S) が成り立つ．
定理 1.49 (Resolution Theorem). S がクローズからなる任意の有限集合であるとき，S が充足不可能であるのは，ある n ≥ 0 に対して，R n (S) が □ を含むときであり，そしてそのときに限る．
定理 1.50 (Unification Theorem). A は WFE の有限かつ空でない任意の集合とする．A が統合可能であれば A は最汎統合子 σA によって最汎統合可能である．なおかつ A の任意の統合子 θについて，ある置換 λ が存在し，θ = σA λ が成り立つ．
補題 1.51. S はクローズからなる任意の集合，P は HS の任意の部分集合とする．このとき R(P (S)) ⊆P (R(S)) が成り立つ．
定義 1.52 (包摂Subsumption). C, D が空でない二つの異なるクローズであり，ある置換 θ について，Cθ ⊆ D が成り立つとき，C は D を包摂するという．
注意 1.53. クローズをそこに含まれるリテラルからなる選言と同一視したとき，二つのクローズ

C, D の間に集合としての包含関係 C ⊆ D が成り立つならば，リテラルの選言としての論理的帰結関係 C |= D が成り立つ．
事実 1.54. C を任意の統合可能なクローズとし，σC をその最汎統合子であるとする．このときC の任意の統合子 θ について，CσC は Cθ を包摂する．
注意 1.55. C が D を包摂するとき，「C は D よりも一般的である」と言うことにすれば，上の事
実は，最汎統合子によって統合されたクローズは，他のいかなる統合子によって統合されたクロー
ズよりも一般的である，と言い換えることができる．最汎統合子という名前はこの性質に由来している．

9

RP と反証

1.5

定義 1.56 (レゾルーション原理（RP）). 任意の二つのクローズ C と D から C と D のリゾル
ヴェントを推論してよい．

RP は Robinson の体系の唯一の推論規則である．
定義 1.57 (反証refutation). クローズの有限列 B1 , . . . , Bn が以下の条件 (a)(b) を満たすとき，この列はクローズの集合 S の反証であるという．

(a)

各 Bi（1 ≤ i ≤ n）について，Bi は S の要素であるか，この列の前にある二つのクローズのリゾルヴェントであるかのどちらかである．

(b)Bn は □ である．

Resolution Theorem から直ちに，クローズからなる有限集合 S が充足不可能なのは，S の反証が存在するときであり，そしてそのときに限る，ということが導かれる．したがって Resolution

Theorem はこの体系における完全性定理である．
例 1.58. 集合 A が次のような二つのクローズ，C1 と C2 を含んでいる．

C1 = {Q(x, g(x), y, h(x, y), z, k(x, y, z))}C2 = {¬Q(u, v, e(v), w, f (v, w), x)}
このとき A は反証 C1 , C2 , □ を持つ．⟨C1 , C2 ⟩ はキー・トリプル ⟨C1 , C2 , N ⟩ を持つことに注意せよ．ただしここで N は次の二つの原子式を含む集合である．

Q(x1 , g(x1 ), x2 , h(x1 , x2 ), x3 , k(x1 , x2 , x3 ))Q(y1 , y2 , e(y2 ), y3 , f (y2 , y3 ), y4 )これらは C1 , C2 に含まれるリテラルもしくはその補式にそれぞれ x-標準化，y-標準化を施して得られた原子式である．N を最汎統合する最汎統合子 σN は，統合アルゴリズムを以下のように遂行することで得られる．

1. σ0 = ϵ, k = 0．
2. B0 = {x1 , y1 }, σ1 = σ0 {y1 /x1 }.
3. N σ1 = {Q(y1 , g(y1 ), x2 , h(y1 , x2 ), x3 , k(y1 , x2 , x3 )),Q(y1 , y2 , e(y2 ), y3 , f (y2 , y3 ), y4 )}.
4. B1 = {y2 , g(y1 )}, σ2 = σ1 /{g(y1 )/y2 }.
5. N σ2 = {Q(y1 , g(y1 ), x2 , h(y1 , x2 ), x3 , k(y1 , x2 , x3 )),Q(y1 , g(y1 ), e(g(y1 )), y3 , f (g(y1 ), y3 ), y4 )}.
6. B2 = {x2 , e(g(y1 ))}, σ3 = σ2 {e(g(y1 ))/x2 }.

10

7. N σ3 = {Q(y1 , g(y1 ), e(g(y1 )), h(y1 , e(g(y1 ))), x3 , k(y1 , e(g(y1 )), x3 )),Q(y1 , g(y1 ), e(g(y1 )), y3 , f (g(y1 ), y3 ), y4 )}.
8. B3 = {y3 , h(y1 , e(g(y1 )))}, σ4 = σ3 {h(y1 , e(g(y1 )))/y3 }.
9. N σ4 = {Q(y1 , g(y1 ), e(g(y1 )), h(y1 , e(g(y1 ))), x3 , k(y1 , e(g(y1 )), x3 )),Q(y1 , g(y1 ), e(g(y1 )), h(y1 , e(g(y1 ))), f (g(y1 ), h(y1 , e(g(y1 )))), y4 )}.
10. B4 = {x3 , f (g(y1 ), h(y1 , e(g(y1 ))))}, σ5 = σ4 {f (g(y1 ), h(y1 , e(g(y1 ))))/x3 }.
11. N σ5 = {Q(y1 , g(y1 ), e(g(y1 )), h(y1 , e(g(y1 ))), f (g(y1 ), h(y1 , e(g(y1 )))),k(y1 , e(g(y1 )), f (g(y1 ), h(y1 , e(g(y1 )))))),Q(y1 , g(y1 ), e(g(y1 )), h(y1 , e(g(y1 ))), f (g(y1 ), h(y1 , e(g(y1 )))), y4 )}.
12. B5 = {y4 , k(y1 , e(g(y1 )), f (g(y1 ), h(y1 , e(g(y1 )))))},
σ6 = σ5 {k(y1 , e(g(y1 )), f (g(y1 ), h(y1 , e(g(y1 )))))/y4 }.
13. N σ6 = {Q(y1 , g(y1 ), e(g(y1 )), h(y1 , e(g(y1 ))), f (g(y1 ), h(y1 , e(g(y1 )))),k(y1 , e(g(y1 )), f (g(y1 ), h(y1 , e(g(y1 ))))))}.
14. B6 = ∅, σN = σ6 .
このとき C1 ξC1 σN と C2 ηC2 σN はシングルトンで，その要素は互いに補式になっている．

2

機械学習における RP の応用
レゾルーションは，クローズの集合 S からリゾルヴェント C を導出する規則である．S のある部分集合 {C1 , C2 } が与えられたとき，これに対してリゾルヴェントは存在しないかもしれないし，複数存在するかもしれない．しかしいずれにせよこの導出の手続きは有限である．特に C1 , C2 のどちらかがシングルトンの場合はこの手続きは決定的 determinisitic なものになる．この推論の過程を逆にして，C1 と C が与えられたとき，C1 と C2 のリゾルヴェントが C になるような C2 を導出するような機械的な手続きが与えられるだろうか？

この過程には定項を変項に変えるという操作が含まれる．したがってこれは具体的な対象に関するデータが与えられているときに，その前提となる一般的な仮説を構築する手続きと考えられる．このような手続きが与えられるならば，
それはベーコン的な帰納法を指示する強い根拠を与えるだろう．ただし気をつけなければならな
いのは，S が充足可能であれば，C も充足可能であるのに対して．この逆は必ずしも成り立たな
いので，ここにおいても仮説が反証されるかどうかのテストが不可欠だということである．
当然予想されることであるが，このような手続きは完全に決定的にはならない．しかしながら様々な制約をつけることで非決定性を減らすことは出来る．それらの制約はいわばヒューリスティッ
クとして機能するものである．

11

2.1

逆レゾルーション

Muggleton と Buntine は RP を逆転させた過程によって一階述語を新しく「発明」する CIGOLというシステムを作った（この名前は LOGIC のつづりを逆にしたものである）．以下，Muggleton

and Buntine (1997) を部分的に要約する．
定義 2.1 (場所). 項あるいはリテラル，あるいはそれらの列の中に項が現れる場所は次のように再帰的な仕方で定義される．

(i)f (t1 , ..., tn ) の中の場所 ⟨a1 ⟩ にある項は ta1 である．

(ii)

f (t1 , ..., tn ) の場所 ⟨a1 , ..., am ⟩ にある項は ta1 の中の場所 ⟨a2 , ..., am ⟩ にある項である．

定義 2.2 (逆置換). t は何らかの項あるいはリテラルであり，θ はある置換であるとする．このとき，tθθ−1 = t であるとき，θ−1 は θ の逆置換であるといわれる．
例えば θ = {t1 /v1 , ..., tn /vn } であるとするとこの逆置換は，

θ−1 = {v1 /(t1 , {p1,1 , ..., p1,m1 }), ..., vn /(tn , {pn,1 , ..., pn,mn })}と表される．ただし pi,mj は t 中の変項 vi の場所を表している．
例 2.3. L = likes(x, brother(x)), θ = {john/x} とすると，

Lθ = likes(john, brother(john)), θ−1 = {x/(john, {⟨1⟩, ⟨2, 1⟩})}
ここで ⟨1⟩, ⟨1, 2⟩ は，L の中の変項 x の現れる場所を表している．
定義 2.4 (θ-差). 二つの項もしくはリテラル t1 , t2 が共通の変項を持っていないとする．このとき，

t1 θ = t2 であり，かつ domain(θ) ⊆ vars(t1 ) であるとき，置換 θ を t1 と t2 の θ-差と呼ぶ7 ．それ以外の場合は差は未定義である．差が定義されているとき，それを中置関係 θ = t1 −θ t2 として表す．実際に二つの項の間の θ-差は一意的であり，以下のように再帰的な仕方で定義される．

(i)
(ii)

v1 −θ t2 = {t2 /v1 }v1 が変項．
∪
f (r1 , ..., rn ) −θ f (s1 , ..., sn ) =(ri −θ si )if

if

f が n 度の述語もしくは関数記号．

1≤i≤nt1 −θ t2 が定義されているとき，t1 は t2 を包摂するという．
注意 2.5. ここで定義された項またはリテラルの間の包摂の概念と，前節で定義されたクローズの間の包摂の概念との間には次のような関係がある．C, D はクローズの空でない集合であり，C ={L1 , ..., Ln }, D = {L′1 , ..., L′m } とする．C が D を前節の意味で包摂するのは任意の Li についてある L′j が存在して，Li が L′j をここでの意味で包摂するときであり，そしてそのときに限る．
7

θ が置換であるとき，θ に属するすべての構成要素の変項の集合を θ のドメインといい，domain(θ) と書く．また任意の表現 e に含まれる変項すべての集合を vars(e) によって表す．また表現からなる任意の集合 E = {e1 , ..., en } に∪ついて vars(E) = 1≤k≤n vars(ek ) とする．

12

例 2.6. 項 t1 = plus(x, y) は項 t2 = plus(3, 4) を包摂する．というのも t1 −θ t2 = {3/x, 4/y} と定義されるから．
レゾルーションの定義を少し修正して述べておこう．C1 , C2 はクローズとする．L1 , L2 はそれ
ぞれ C1 , C2 に属するリテラルであり，L1 と L2 が最汎統合子 θ を持つものとする（定義 1.9 参照）．
このとき C = (C1 − {L1 })θ ∪ (C2 − {L2 })θ を C1 と C2 のリゾルヴェントといい，C1 • C2 と書く．
置換 θ は θ = θ1 θ2 かつ domain(θ1 ) ⊆ vars(C1 ) かつ domain(θ2 ) ⊆ vars(C2 ) を満たすような，構成部分 θ1 , θ2 に一意的に分解される．ここからC = (C1 − {L1 })θ1 ∪ (C2 − {L2 })θ2

(1)が得られる．
レゾルーションは理論（ここではクローズの集合と考える）から帰結を導き出すのに使われる．
ある理論 T について，L が T の帰結であるのは T ∪ {L} が充足不可能であると示されるときであり，そしてそのときに限る．前章の定理 1.49 より，これは T ∪ {L} に RP を有限回適用して反証が得られることと同値である．
例 2.7. 理論 T はクローズ C1 = {larger(hammer, f eather)}, C2 = {denser(hammer, f eather)}, C3 ={heavier(x, y), ¬denser(x, y), ¬larger(x, y)} からなるものとする．C = {heavier(hammer, f eather)}
が T の帰結であることをは次のように示される．まず C3 と {¬heavier(hammer, f eather)} から

RP によって，C4 = {¬denser(hammer, f eather), ¬larger(hammer, f eather)} が得られる．次に C2 と C4 から RP によって C5 = {¬larger(hammer, f eather)} が得られる．最後に C1 と C5から □ が得られる．したがって T ∪ C には反証が存在する．T は明らかに充足可能なので，T から heavier(hammer, f eather) が帰結することが分かる8 ．

CIGOL は例から理論を構築する三つのタイプの演算子を使っている．
「V」演算子は新しい述語を導入せずにすでに存在しているクローズを一般化する．
「W」演算子は新しい補助的な述語を導入する．短縮演算子は Plotkin の最小一般化の関係（least general generalization relation）を適用することで単位クローズを生み出す，「W」演算子の境界事例である．ここでは「V」演算子を取り上げる．

2.1.1「V」演算子Figure 3 はいくつかの「V」が繋がったものとみることができる．Figure 4 はこれらの「V」の一般的な形式を示している．RP は「V」の腕の先にある二つのクローズから，「V」の下にあるクローズを導出する規則である．ここで説明されるメカニズムは逆に腕の一方にあるクローズと底にあるクローズから，もう一方の腕にあるクローズを導出するものである．Figure 4 では RP をかけられる C1 のリテラルは正 (+)，C2 のリテラルは負 (−) である．
8

Figure 3 参照．

13

C1 , C2 を含むどんな理論においても C は余分である．というのもそれは C1 , C2 から直接的に含意されるからである．C は廃棄することができるという事実より，「V」演算子は理論の単純化と簡略化を可能にする．

Figure 4 の C1 と C から C2 を構成する操作を吸収といい，C2 と C から C1 を構成する操作を同定という．この二つの操作をあわせて「V」演算という．フォーマルな定義は後に出される．以下
では吸収の過程を説明する．吸収の操作によって C1 と C から導出されるクローズ C2 を，レゾ
ルーションの商といい，C2 = C/C1 と書くことにする．
二つのクローズから RP によって導出されるクローズの数は有限であり，特にレゾルーションを受けるリテラルが決まれば，そのとき導出されるクローズは一つに決まる．しかしながら二つの与えられたクローズ C1 , C に対して，C1 と RP によって C を導出できるようなクローズは無限にある9 ．そこで吸収の操作は，いかにしてそこから非決定性を減らすかがポイントになる．そのために操作を受けるクローズにはいくつかの制約が課される．
二つのクローズが共通のリテラルを持たないとき，この二つのクローズは分離可能であるという．RP を適用される二つのクローズに関して，以下では常に分離可能性が前提されているものとする．基礎ホーン・クローズ（p. 5，定義 1.11 参照）のケースでは，分離可能性を想定すれば，レゾルーションの商は一意的に決まる．一階のクローズでは一般的に商は一意的には定まらない．
しかし等式 (1) について考察することで，私たちはこの商に対する正確な制約を見つけることができる．(1) に対する単純な代数的操作によって次の等式が得られる．

C2 = (C − (C1 − {L1 })θ1 )θ2−1 ∪ {L2 }(2)

さて θ1 θ2 は L1 と L2 の最汎統合子だから，L1 θ1 = L2 θ2 である．したがって，

L2 = L1 θ1 θ2−1

(3)(3) を (2) に代入することによって，
C2 = (C − (C1 − {L1 })θ1 )θ2−1 ∪ {L1 }θ1 θ2−1=((C − (C1 − {L1 })θ1 ) ∪ {L1 }θ1 )θ2−1(4)が得られる．C と C1 が与えられたとき，等式 (4) において非決定性の源は三つある．L1 , θ1 , θ2−1
である．この非決定性を減らすために C1 がシングルトンであると仮定する．つまり C1 = {L1 } とする．これによって (4) は C2 = (C ∪ {L1 }θ1 }θ2−1 に単純化され，非決定性は θ1 と θ2−1 の選択に減らされる．

θ2−1 を決定的でなく構成することを考えてみよう．逆置換の定義により，私たちは (C ∪ {L1 }θ1 )の中のどの項が異なる変項に写像されるかを決めなければならない．C に現れる項 t と，{L1 }θ1
次のような状況と類比的に考えればよい．集合 A, B が与えられたとき A ∩ B は一意的に決まる．しかし A, C が与えられたとき，A ∩ B = C となるような B は無限に存在し，一意的には決まらない．
914

に現れる t1 θ1 は，θ2−1 に現れるのと同一の変項 v に写像されるとする．ただしここで t1 は {L1 } の項とする．このことは t1 θ1 = t を含意する．明らかにこの場合 t1 −θ t は定義されており，θ1 の部
分集合である．これは C と C1 = {L1 } が与えられたときに C2 を仮説として立てる，決定的でないアルゴリズムを示唆している（Argorithm 1)．Algorithm 1 において，集合 S の分割 Π というのは共通部分をもたない集合の集合であり，要素になっている集合（ブロックという）の和が Sに等しくなるようなものを意味している．つまり例えば S = {a, b, c} に対して，{{a}, {b, c}} は Sの一つの分割である．

Algorithm 1: 吸収を計算する非決定的アルゴリズム
Input: クローズ C と C1 = {L1 }T P = {(t, p)|t は (C ∪ {L1 }) の場所 p にある項 } であるとせよ．
T P ′ は T P のある部分集合であるとせよ．
T P ′ の分割 Π を以下のように構成せよ．
Π のそれぞれのブロック B = {(r, p1 ), ...(r, pn )} ∪ {(s, q1 ), ..., (s, qm )} は
次のようなものであるとせよ．

s は r を包摂し，すべての (r, pi ) は C の項に対応し，(s, pj ) は {L1 } の項に対応する．
∪
上のすべてのブロック B に対して θ1 = (s −θ r) とせよ．
θ2−1 = {(r, {p1 , ..., pn , q1 , ..., qm })/v| 上のすべてのブロック B に対して } とせよ．
ただし v はすべて異なる変項で，(C ∪ {L1 }) にはないものとする．

Output: C2 = (C ∪ {L1 }θ1 )θ2−1
Algorithm 1 は非決定的なので，これを実行するには捜索ベースのアルゴリズムとして定式化しなおさなければならない（省略）．これは単純性と簡略性をヒューリスティックとして用いる．
例 2.8. C = {x < s(s(x))} とし，C1 = {y < s(y)} とする．ただし s(z) は z の後続者を意味する．
このとき(C ∪ {L1 }) = {x < s(s(x)), ¬(y < s(y))},T P = {(x, ⟨1, 1⟩), (x, ⟨1, 2, 1, 1⟩), (s(x), ⟨1, 2, 1⟩),(s(s(x)), ⟨1, 2⟩), (y, ⟨2, 1⟩), (y, ⟨2, 2, 1⟩), (s(y), ⟨2, 2⟩)}.
T P ′ は非決定的に {(s(s(x)), ⟨1, 2⟩), (s(y), ⟨2, 2⟩)} とする．Π は自明な分割 {{(s(s(x)), ⟨2, 2⟩)}} とする．このとき，

θ1 = {y/s(x)},θ2−1 = {(s(s(x)), {⟨1, 2⟩, ⟨2, 2⟩})/z},
C2 = {(x < z), ¬(s(x) < z)}.
これは確かにレゾルーション関係 C = C1 • C2 を満たす．

15

参考文献

Gabbay, Dov M., Hogger, C. J. and Robinson, J. A. (eds.): Handbook of Logic in Artificial
Intellignece and Logic Programming. Vol. 1. Logical Foundations, Clarendon Press, 1993.
Mendelson, E: Introduction to Mathematical Logic, fourth edition, Chapman & Hall, 1997.
Muggleton, S: Inductive logic programming. Muggleton (ed.) Inductive Logic Programming,
Academic Press, 1992, pp. 3-27.
Muggleton, S and Buntine, W.: Machine invention of first-order predicates by inverting resolution. Muggleton (ed.) Inductive Logic Programming, Academic Press, 1992, pp. 261-280.
Plotkin, G. D.: A note on inductive generalization. Bernard Meltzer and Donald Michie (eds.),
Machine Intelligence 5, Edinburgh University Press, 1969, pp. 153-163.
Robinson, J. A.: A machine-oriented logic based on the resolution principle. Journal of the
Association for Computing Machinery, 12, no. 1 (January, 1965), pp. 23-41.

16