自動定理証明と応用 (automated theorem proving and its application)

Presentation on theme: "自動定理証明と応用 (automated theorem proving and its application)"— Presentation transcript:

1 自動定理証明と応用 (automated theorem proving and its application)
認知システム論　知識と推論（６） 知識と論理で問題を解決する 自動定理証明と応用 (automated theorem proving and its application) 代入， 単一化，融合 自動定理証明と質問応答システム

2 (substitution, unification, and resolution)
代入，単一化，融合 (substitution, unification, and resolution)

3 代入，単一化，融合の概要 ソクラテスは人間である 人間は死ぬ運命にある 単一化 代入 融合 ソクラテスは死ぬ運命にある
　今回は，命題論理で学んだ「融合」（レゾリューション）という推論規則を一階述語論理でも使えるようにする．このスライドはその概略である． 　まず，節に含まれている変数（x など）は，暗黙に全称記号（∀）で限量されたものであることを思い出そう．したがって，x をどんなオブジェクトで置き換えても，その節は真である．そこで，x をSocratesに置き換えてみる．このように，変数を項に置き換える操作を代入という． 　この代入によって，一方の節には HUMAN(Socrates)，他方の節にはそれに否定記号を付けた ￢HUMAN(Socrates) が含まれるので，「融合」によってこれらをキャンセルし，残りの節をつないだ節を融合節として生成できる．この例の場合，それは MORTAL(Socrates)．したがって，「ソクラテスは死ぬ運命にある」ことが導出できた． 　明らかに，ここでの技術的ポイントは，「x をSocratesに置き換えた」代入にある．なぜ，この代入を発見できたのだろうか？　それは， 他の節に含まれている HUMAN(Socrates) と，それと異符号で同じ述語記号をもつ￢HUMAN(x) を見比べて，x と Socrates が対応することに気が付いたからである．このような変数を含まない「データ」と変数を含む「パターン」を見比べる操作は，一般に，パターン照合と呼ばれているが，一階述語論理では，それをさらに強力にした「パターン」と「パターン」を見比べる「単一化」という操作を用いる． 　以下のスライドでは，準備として「代入」に関する予備知識を身に付けた後，「単一化」のアルゴリズムを使うことにより，命題論理の「融合」を一階述語論理の推論操作に拡張できることを学ぶ．その後，その応用として，自動定理証明と質問応答システムの基本的な設計法について学ぶ． 融合 ソクラテスは死ぬ運命にある

4 代入(1/4) 代入 変数 を項 に同時に置き換えることを表す 例 x y a g(z)
変数　　　　　　　を項　 に同時に置き換えることを表す 例 x y a g(z) 　「代入」(substitution)は，このスライドのように，「変数」と「項」の対「変数／項」を集めた集合である．これにより，「変数」をそれに対応する「項」に置き換える操作を表している．この表記法はやや見にくいが，このスライドの例に示したような表形式のデータを１行で表しているものだと思えばよいだろう．ふつうのプログラミング言語の「代入文」とやや似ている点もあるが，基本的に別物と考えておこう．

5 代入(2/4) 代入の（項 t への）適用 項 t 内のすべての変数に対して，σで指定された置き換えを同時に一回のみ行った結果を表す 例 x
y a g(z) 　代入σで指定された変数の置き換えを項ｔに（同時に１回）適用して得られる項をσ(ｔ)と表す．

6 代入(3/4) 代入σは，項の集合T からTへの関数 σ: T → T とみなすことができる 代入の合成
　 σ(ｔ)の表記法からわかるように，代入σは項を受け取り項を返す関数と見なすことができる．すると，数学でよく知られた「関数合成」によって，代入の合成を定義することができる．すなわち，項ｔにまずσ2を適用して項ｕを得て，そのｕにσ1を適用して項ｓが得られるとき， ２つの代入σ1とσ2を合成した１つの代入（σ1○σ2）とは， （σ1○σ2）(ｔ)＝ｓ によって，ｔからｓを１度の置き換えで得られる代入である．その例はつぎのスライドで．

7 代入(4/4) 代入の一般性 代入σは，代入σ’ より一般的である(more general) ある代入τに対し，
　このスライドは，代入の合成を図で示したものである． 　項g(x,y)に代入σを適用すると，項g(y,y)になる．そこでさらに代入τを適用すると，項g(b,b)となる． 　ここで得られた項g(b,b)というのは，最初の項g(x,y)に代入σ’を１回適用しても得られる．したがって， 代入σ’は，２つの代入τとσの合成である． 　ここで，２つの代入のうち，一方が他方に比べて，「より一般的である」(more general)という概念を導入する．その定義はスライドにあるとおりである．直感的に言えば，代入σに対して他の代入を合成すると，より一般的でなくなる．つまり，less general あるいは more specific になる．代入を合成すると，任意のオブジェクトを表していた変数が，特定のオブジェクトに置き換えられる可能性があるからである． ある代入τに対し，

8 単一化 (1/7) 　単一化(ユニフィケーション)の定義をする．２つの項ｓ，ｔが与えられたとする．その中に含まれている変数を適切な項で置き換えて，２つの項を同一（単一）のものとしたい．その処理が単一化である．変数を適切な項に置き換えることを代入σで表すと，σ（ｓ）＝σ（ｔ）ということになる．このσを単一化子（ユニファイア）という．また，このとき，２つの項は単一化可能である．単一化可能でなければ，単一化不能である． 　一般に，単一化子は複数個存在し得る．その中で，すでに学んだ「より一般的」(more general)という概念のもとで「最も一般的」(most general)なものを最汎単一化子(most general unifier)といい，単にmguということもある．２つの項が与えられたとき，そのmguは，実質的には，ただ１つしかない．（「実質的には」の意味は，変数名を適当に付け替えれば，見かけ上それとは異なるmguを作れる場合があるからである．たとえば，f(x)とf(y)のmguは，{x/y}や {y/x}がある．）

9 単一化(2/7) mgu 例 単一化 mguではない
　この例では，σ’は単一化子である．しかし，mguはσである．なぜなら， σ’ を適用して得られる項f(h(a),g(h(a)))は，σを適用して得られる f(h(y),g(h(y))) に代入τ={y/a}を適用すれば得られるからである．

10 単一化 (3/7) s t 単一化アルゴリズム 【入力】 項 s,t
【出力】　項 s,t が単一化可能ならばmguを出力． 　　　　　　　　　　　単一化可能でなければ「失敗」を出力． 【手順】　関数記号を解釈しない方程式 s = t を変形し， 　　　　　x = t の形の方程式を導出して，代入を構成する． s t 方程式 　単一化アルゴリズムとは，入力された項ｓ，ｔの単一化を試み，単一化可能ならmguを出力し，単一化不能ならそれを表す「失敗」という情報を出力するものである． 　具体的な処理手順は，いろいろなものが提案されている．この授業では，特定のアルゴリズムを示すことはせず，すべてのアルゴリズムの共通的，本質的な考え方を学ぶ． 　そのポイントは，問題をｓ＝ｔというような方程式で表現することである．変数への代入を求めて左辺と右辺を等しくするというのは，まさによく知られた「方程式を解く」という概念そのものだからである．ただし，この方程式には足し算も掛け算も出てこない．見かけ上，「関数記号」が出てくるが，それは何の計算もしない，単なる文字列である． 　つぎのスライドで示す手順により，この方程式は分解され，複数の方程式群，すなわち連立方程式のようになっていく．これが正規形（どの方程式も，左辺が変数，右辺がその変数へ代入すべき項）となれば，それが解，すなわち，mguを表すこととなる． 解

11 単一化 (4/7) 出現検査 例： x = f(x) x は変数，t は項を表す
　このスライドに示された６つの方程式変形ルールが単一化アルゴリズムの本質を表している．これらのルールは，適用可能な方程式が連立方程式に含まれていれば，いつでもどこにでも何度でも適用してよい． 　（１）両辺のトップ（左端）の関数記号が等しい方程式があれば，この方程式を削除し，対応する引数同士を等しいと置いた方程式群を追加する．（問題の簡約化） 　（２）両辺のトップの関数記号が異なる方程式があれば失敗．与えられた２つの項は単一化不能である．（変数は置き換えられるが，関数記号は置き換えられないので，関数記号が異なればアウト．）なお，ここでは，固体記号（定数）は，引数が0個の関数記号とみなしている．したがって，f(x)=a のときなども失敗となる． 　（３）ｔ＝ｘという形の方程式は，両辺を入れ換えてｘ＝ｔとする．ただし，ｘが変数で，ｔが変数ではない場合．（最終的な解はこういう形にしたい．） 　（４）ｘ＝ｘという形の方程式は削除する．（自明に成り立っているので．） 　（５）ｘ＝ｔ（ｘが変数で，ｔが変数ではない）という形の方程式は，ｘがｔの中に出現しているかどうかで２通りのいずれかの処理を実行できる． 　　　（５Ａ）ｘがｔの中に出現している場合は失敗．与えられた２つの項は単一化不能である．（これは，出現検査(occur check)と呼ばれている．変数を何に置き換えても両辺を同じにできないことは自明．） 　　　（５Ｂ）ｘがｔの中に出現していない場合，他の方程式に出現しているｘをｔで置き換える．（数学で習う連立一次方程式の解法でも，ふつう，同様な代入を行う．）

12 単一化 (5/7) 　以上のどのルールも適用できなくなったときの連立方程式は，そのままで解（mgu）を表している．形式を整えて，代入σの形にする．

13 単一化 (6/7) 例 　単一化アルゴリズムの適用例である．もちろん，アルゴリズムはどのルールをどの方程式に適用するかはまったく自由（すなわち，非決定的）なので，このスライドで示した筋道以外にも，解に至る道がある．

14 単一化 (7/7) 例 単一化不能 単一化不能 　ここに単一化の概念を確認するための小さな例を８つ示す． 単一化不能 単一化不能

15 融合(1/3) 命題論理の場合 融 合 (resolution) 節に対して適用する推論規則 融合節
符号だけが異なる２つのリテラル（相補リテラル）を１個ずつキャンセルし，残りのリテラルを∨で結合する． ただし，重複したリテラルは１個を残して削除する． ∨は交換則と結合則を満たすので，キャンセルするリテラルの節の中の場所はどこでもよい． 　これは，命題論理のところですでに学んだ「融合」（レゾリューション）の説明図である． 　２つの論理式 　　　Ｐ∨Ｃ　(1) 　　　￢Ｐ∨Ｄ　(2) が与えられたとしよう．(1)の一部には変数Pが含まれていて，(2)の一部にはその否定( ￢Ｐ）が含まれている．この２つのリテラル（Ｐと￢ P） は，実際には，このスライドのように左端に現われている必要はない．節はリテラルを∨ で結合したものであり， ∨は交換則と結合則により，その結合の順番を変えたり入れ換えたりしても等価だからである． 　このような状況になっているとき，(1)からＰを除去し，(2)から ￢Pを除去して，残りのリテラルを∨で結合したもの 　　　Ｃ∨Ｄ　(3) は，やはり，節の形をしている．これを(1),(2)から得た融合節と呼ぶ． 　このように，(1)と(2)から融合節(3)を生成する推論規則を融合という．Pを正リテラル，￢ Pを負リテラルという．この正負のことをリテラルの符号という．また，このように符号だけが異なり，他の部分はまったく同じ２つのリテラルを相補リテラルという． 　この言葉を使って表現すると，融合とは，２つの節から相補リテラルを１個ずつキャンセル（削除）し，残りのリテラルを∨ で結合するアルゴリズムであるということができる．

16 融合(2/3) 一階述語論理の場合 ソクラテスは人間である 人間は死ぬ運命にある 単一化 代入 融合
　融合の考え方は，一階述語論理にも適用できる．ただし，単一化によって適切な代入を求め，それを節に適用することによって相補リテラルを作り出してから，相補リテラルを削除し，残りの部分を∨で結合する．このスライドの例では，HUMAN(Socrates) と ￢HUMAN(x) は相補リテラルではないが，符号を除いた部分を単一化することによって，mguを求め，それを適用することによって，相補リテラルHUMAN(Socrates) と ￢HUMAN(Socrates) を得ている． 融合

17 融合(3/3) 変数名の付け替え 節の中の変数名は，他の節のものと異なるように，名前を付け替えること．
　１つだけ注意がある．同じ変数が異なる節で使用されていても，本来それらは別々の意味をもつ変数である．したがって，単一化するまえに，一方の節の変数名を適切に付け替える必要がある．

18 休憩

19 (automated theorem proving and question-answering system)
自動定理証明と質問応答システム (automated theorem proving and question-answering system)

20 自動定理証明(1/3) 結論を否定し，空節を導出する
公　理 証明なしで認める 事実や規則 定　理 公理から導かれる 論理的帰結 定理の仮定 定理の結論 否定 節集合　KB 節集合　Q 　定理とは，証明なしで認める事実や規則を表す公理から導かれる論理的帰結のことであり，ふつうは，仮定と結論からできている．たとえば，中学校で習うユークリッド幾何学では「異なる２点を通る直線はただ１本存在する」というのが幾つかある公理の１つである．また，定理は無数にあり，たとえば，「二等辺三角形の２つの底角は等しい」というものがある． 　公理と定理が一階述語論理で表現されている場合，これをコンピュータで自動的に証明するにはつぎのようにする． 　１．公理および仮定を節集合にする．それをＫＢとしよう． 　２．結論の否定を節集合にする．それをＱとする． 　３．ＫＢとＱの和集合Ｓが充足不能なら定理は真である．それを示すため，融合原理を用いて，Ｓから空節を導出する．Ｓから空節に至る節の系列を証明と呼ぶ． KB ∪ Q から空節が導かれれば， KB ∪ Q は充足不能なので， 定理が証明できたことになる

21 自動定理証明(2/3) 代数系の例題 単位元が存在し，結合則を満たす代数系において，もし各要素の２乗が単位元になるならば，その系は交換則を満たす． 単位元が存在 結合則を満たす 各要素の２乗が単位元 　数学の代数学の分野から自動定理証明の例題を１つ示す． 　ある集合の要素に関する演算を考える．それを仮に「積」と呼び，演算子を・で表す．たとえば，x と y の積が z であるとき，x ・y = z である． 　単位元とは，任意の x に対し， e ・x = x ・e = x を満たす要素のことである． 　結合則は，任意の x, y, z に対し， (x ・y) ・ z = x ・(y ・ z ) が成り立つ性質のことである． 　証明したいことは，単位元が存在し，結合則を満たす演算は，もし各要素の２乗が単位元になる( x ・x = e)ならば，交換則を満たす，すなわち，任意の x, y に対し， x ・y = y ・x が成り立つことである． 　この問題を一階述語論理で記述するために，P(x,y,z) でx ・y = z であることを表す． 　結合則の記述がやや複雑だが， 　　「任意のx,y,z,u,v,w に対し， x ・y = u かつ y ・ z = v ならば， u ・ z = w ←→ x ・ v = w 」 を節集合に変換すると得られる． 　交換則は，(∀x)(∀y)( P(x,y,z) →P(y,x,z) ) なので，その否定を節集合に変換する． 　　　￢(∀x)(∀y)( P(x,y,z) →P(y,x,z) ) = (∃x) (∃y) (∃z) ￢ ( P(x,y,z) →P(y,x,z) ) = (∃x) (∃y) (∃z) ￢ (￢ P(x,y,z) ∨P(y,x,z) ) = (∃x) (∃y) (∃z) (P(x,y,z) ∧ ￢ P(y,x,z) ) 　これをスコーレム標準形に変換すると，スコーレム定数 a,b,c を導入して， P(a,b,c) ∧ ￢ P(b,a,c) となるので，スライドに示した２つの節が得られる． 交換則を満たす（の否定）

22 自動定理証明(3/3) 証明の例 (6)と(4)の1番目のリテラルを融合
　これがその証明の例である．もともとの７つの節を含めて130個の節を生成した後に空節を導出できている．この証明の中で使われていない１１４個の節は，無駄な節であったことになる．（ただし，これ以外の証明（別解）には使えるかもしれないが．）一般にこのような無駄はある程度はどうしても出てしまうのだが，なるべく少なくするような工夫が行なわれている．

23 質問応答システム(1/7) Yes/No-質問
知識ベース　ＫＢ (1) 人間は死ぬ運命にある (2) ソクラテスは人間である 質問 ソクラテスは死ぬ運命にあるか？ (3) 推論 (1),(2),(3) から空節が導かれる 　つぎに，人工知能を用いた一般性のある質問応答システムの基本的な設計法を学ぼう．異なる３種類の質問に分けて考える． 　１つめの質問のタイプは，Yes/No型の質問である．それに答えるには，質問の内容（Yesであるときの叙述）の否定を知識ベースに加えて推論させ，空節が導かれればYesと応答すればよい．絶対に空節が導かれないなら No と応答する． 　ただし，一般には，時間がいつまでたっても推論が終了しないこともある．そのときには，適当な時間で打切って，I’m sorry I don’t know. などと応答することになるだろう． 応答 YES

24 質問応答システム(2/7) Wh-質問 Who, Where, What などの質問に，オブジェクトを答える 知識ベース ＫＢ (1)
知識ベース　ＫＢ (1) Mary はJohn の妻である オントロジー 「妻」と「夫」の関係 (2) 質問 だれが Mary の夫か？ ANS 述語の引数に解を求める (3) （zがMaryの夫ならば，zが答えである） 推論 　２つめの質問のタイプは，「だれ」，「どこ」，「なに」等を質問する，いわゆる，Wh-型の質問である．この質問の答えるためには，特別な述語 ANSを用意する．ANS(x)は，「xが質問の答えである」を意味する．これを利用して，質問の条件を満たすオブジェクトが見つかれば，そのオブジェクトがANSの引数となるように論理式を記述する． 　たとえば，このスライドでは， 　　「MaryはJohnの妻である．」 　　「xがyの妻ならば，yはxの夫である．」 という知識ベースがあるとして，「だれがMaryの夫か？」という質問を与えている． 　この質問の答えを得るために， 　　「zがMaryの夫ならば，zが答えである．」 という節を記述している． 　質問応答システムは，節がANS述語だけを含むように，融合を用いて推論を進めていく．言い換えれば，ANS述語を無視すれば空節となるような節を目指して融合を適用していく． 　知識表現の観点からこの例題で注目すべき点は，知識ベースの中では，「妻」という言葉でデータが蓄積されているにも関わらず，質問では「夫」という言葉を使っていることである．質問応答システムは， という知識によって，「妻」という言葉と「夫」という言葉を関連付けている． 　一般に，このような知識は「オントロジー」と呼ばれており，非常に重要である．オントロジーの別の例として，概念の上位関係を表すものがあり，一般に，is-a 関係と呼ばれている．たとえば，「犬は動物である」というような「犬」と「動物」の関係である．「ポチは犬である」というデータがあるときに，質問として，「動物の例を示してください」（「何が動物か？」）を与えると，オントロジーを用いて，「ポチが動物です」という応答をすることができる． (3),(2)から　　　　　　　　　　　　　　　　　　　　 (4) (4),(1)から　 (5) 応答 John

25 質問応答システム(3/7) How-質問 「行為」を状態遷移関数として表現する How の質問に対して，行動手順を答える 行為 aｃｔ
状態　s 状態　aｃｔ(s) 　最後に，３つめのタイプ，How型の質問を考える．これは，方法や手段あるいは手順を問う質問である．「手順」というのは，「ああして，こうして，．」という内容なので，一言では解答できない．一般には，行為（アクション）の列を順番に並べた状態遷移の系列を答えることになる． 　そのような情報を表現するために，各々の「行為」を状態遷移関数を表す関数記号で表現する．その引数には，状態 s と遷移先の決定に必要な補足情報を含めることとし，返す値は，状態 s でその行為を行なったときの遷移先の状態であると解釈する． 　たとえば，行為 act によって状態が s から s’ に遷移するとき，s’=act(s) などとする．遷移先を決定するのに補足情報 a が必要なら，s’=act(a,s) などとする．

26 質問応答システム(4/7) How-質問（例題）
サルが部屋の天井からつるしたバナナを食べようとしている．サルのできる行為は， 部屋の中を移動すること， 部屋の中にあるイスを持ち運ぶこと， バナナを取るためにイスの上に登ること である．サルはどうすればバナナを取ることができるか？ Banana Chair 　行動心理学の分野で知られている「モンキー・バナナの問題」を例題として考えてみる．その問題はスライドに書かれているとおりである．ここでの問題は，サルがバナナを取る手順を発見することができるようなシステムを設計することである． Ape

27 質問応答システム(5/7) How-質問（例題）
状態 s において，（サル,バナナ,イス）の位置＝(x, y, z)． 状態 s において，サルはバナナを取ることができる． 状態 s でサルが位置vに移動して得られる新状態 　この例題を解くために，PおよびREACHという２つの述語を用意する． 　P(x,y,z,s)は状態sにおけるサル，バナナ，イスの位置を命題として記述する． 　REACH(s)は，状態sがゴールであることを表す． 　サルがとることのできる３つの行為をそれぞれ walk, carry, climb という状態遷移関数で表現する．それぞれの具体的な意味はスライドに書かれたとおりである．いずれも，引数 s で示された状態でその行為をとると，どのような新状態になるかを関数値として示している． 状態 s でサルが位置wへイスを運んで得られる新状態 状態 s でサルがイスに登ったときに得られる新状態

28 質問応答システム(6/7) How-質問（例題）
知識ベース　ＫＢ 各行為と状態遷移の関係を記述する 　各行為によって，状態がどのように変化するかを記述する．ただし，s,v,w,x,y,zはいずれも変数とする． 　（１）状態s=(x,y,z)でvに歩くと，状態はwalk(v,s)=(v,y,z)になる． 　（２）状態s=(x,y,x)（x=zに注意！）でイスをwに運ぶと，状態はcarry(w,s)=(w,y,w)になる． 　（３）状態s=(x,y,x)（x=zに注意！）でイスに登ると，状態はclimb(w,s)=(x,y,x)になる． 　（４）状態s=(x,x,x)（サルとイズがバナナの位置にある）でイスに登った状態 climb(s)がゴールである． 　初期状態は，InitialState=(a,b,c) とする． 　REACH(s)ならば，s が答えである． 初期状態 質問

29 質問応答システム(7/7) How-質問（例題）
　これが導出の例である．応答は，「初期状態からｃへ歩き，そこにあるイスをｂへ運び，そこでイスに登る」という行動手順を表している． 応答