たまに、Prolog ...

なんか今日は学生が少な目なので、予定と違って Prolog をいじってみました。そういえば、

＊　SICStus Prolog が見当たらない

まぁ、SWI-Prolog でいいんだけどね。倍以上速さは違いますが。SWI-Prolog自体は一発で動きました。

Prolog は定理証明と関連して語られることが多いけど、実際には反例を探しにいくのでモデル検査の方に近いです。Haskell の方が Curry Howard 対応があるから証明系に近い。

でも、今から見ると面白いのは線型充足法とか単一化よりも、

＊　任意の論理式を節形式

に落とすところだな。しばらく証明系いじっていたので、そっちの方を面白く思ってきたということなのかも。なんだけど、どうも、そこを授業の資料に書くのは忘れたらしい。どっかの辞書に書いた記憶もあるが。

∀x∃yをスコーレム関数を使ってなくすわけですが、問題解決的にも有効だと思う。節形式への変換プログラムは僕は書いたことないかな。節形式は、

p(X),q(f(Y)) :- r(X),s(g(Y)).

という形式ですけど、Sequent Calculus と同じ。そういえば、Proofs and types にも「Prologと関係あるんだ」とか書かれていた。自然演繹とSequent Calculusを両方やるのは、ちょっと抵抗あるけど。

まぁ、もうプログラミング言語として使うことはないと思うけど…