Prologで論理的にプログラミングを学んでいます（問合せ、回答）

　AI言語Prologによるプログラミング学習の第3回です。テキストは、「地味に論理的」です。
　内容は、Prologにおける問合せとその回答の仕組みです。

問合せ

　問合せとは、例えば「駅Aとnearby関係にある駅はどれか？」というものである。Prologにおける問合せは、以下のように記述される。

?- nearby (駅A, W)　

　ここで、接頭語の'?-'は、問合せである（事実ではない）ことを表す。
　この問合せに対する回答は、以下のように記述される。

{W->駅B}

　これは、変数Wについての値(駅B)の代入を表す。この代入により、問合せの文

nearby (駅A, 駅B)

は真となる。

　nearby関係が事実のリストで定義されている場合、問合せに回答することは容易である。問合せに整合する事実を探し出すだけでよい。

　一方、規則が関連してくる場合、問合せへの回答には複数の工程を実行しなければならない。
　まず、問合せ

?- nearby (駅A, W)

に答えるときには、それを規則

nearby (X, Y) :- connected (X, Y, L)

の結論（ここではnearbyです）に照らし合わせて、代入

{X->駅A, Y->W}

を引き出す。
　次に、この代入を規則に対して行い、そのときの前提（ここではconnectedです）についての回答を探す。すなわち、問合せ

?- connected (駅A, W, L)

に対する回答を探す。
（これは、「任意の路線Lにより駅Aとconnected関係にあるのはどの駅か？」という問合せです。言い換えるなら「駅Aと直接接続されているのはどの駅か？」の問合せです。）

　駅Aと直接接続された駅を発見できたなら、駅Aとnearby関係にある駅を発見したことになる。
　つまり、直接接続についての事実を見つけることで、問合せの回答が得られる。
　例えば、事実から得られた回答を

{W->駅B, L->路線L}

とする。
　ここで、変数Lは最初の問合せには現れない。
　そのため省略され、最終的な回答は

{W->駅B}

となる。

導出

　以上の工程は、一般的な推論のパターンに従う。
　つまり、問合せ

?- $${Q_1, Q_2, …, Q_n}$$

に回答するためには、まず$${Q_1}$$に整合する結論Aを有する規則

$${A\coloneq B_1, …, B_m}$$

を見つける。（所謂カットです。）
　次に問合せ

?-$${B_1, …, B_m, Q_2, …, Q_n}$$

について、同様に回答を見つける。

　この推論パターンは、導出と呼ばれる。導出は、論理式に対して、宣言的解釈（真偽のいずれかの値をとる）の他に、手続的な解釈を加えるものである。

背理法

　導出による証明の過程では、背理法として知られる技術が用いられる。つまり、証明すべき式が偽であると仮定して矛盾が導かれることを示し、それにより実際には与式が真であることを証明する。

　例えば、駅Aとnearby関係にある駅を知りたいとする。この文を否定すると、駅Aとnearby関係にある駅は存在しない、となる。
　これは、論理では、結論が空である規則として表される。つまり、前提が真であることにより偽が導かれる規則である。

$${\coloneq}$$nearby (駅A, W)

（$${\lnot\;p \stackrel{def}{\equiv} p\to\bot}$$のことだと思われます。）

　矛盾があるときは、導出により空規則が導かれる。空規則は、前提が恒真、結論が恒偽である。空規則は、$${\Box}$$として記述される。

　（ここの説明はよく分かりませんでした。もしかしたら、詳しい説明が後ほどにあるのかも知れません。）

グランドと成功集合

　nearby関係についての二つの定義が同じものであることを示すために、グランド事実と成功集合を導入する。
（二つの定義は、nearby関係の事実のリストによる定義と、nearby関係とconnected関係の規則による定義です）

　グランド事実は変数を持たない事実である。
　成功集合は、Gをグランド事実とするときに問合せ

?-G

が成功するようなGの集合である。

　nearby関係の事実はグランド事実であり、かつそれらの事実からは何も演繹されない。したがって、一つ目の定義による成功集合は、事実のリストの要素のみからなる。

　二つ目の定義による成功集合は、上述の規則をconnected関係のグランド事実に適用することで構成される。

　以上から、二つの定義は、それらが同じ成功集合を有するとき、（手続的に）同じであると言える。

練習問題

　私は練習問題に対する驚くべき答案の作成をしたが、その証明木を記述するにはnoteの数式機能は貧弱すぎる。　

---

まとめ

　今回は、後半の説明が分かり難くかったです。特に導出と背理法の関係がよく分かりませんでした。
　また、基礎となる証明体系がはっきりしないので、統語論的な部分の理解に不安があります。
　あと練習問題は、答案作成を証明図でしたのですが、代入を書き込むことができなかったので記載するのを止めました。

　次回は、再帰（もしくは帰納）について学ぶ予定です。