日々の流転

λ. Otter で 3 not problem を解く

20080716#p02で紹介したように、3 not problemを定理証明機のOtterに解かせる例が <URL:http://www-unix.mcs.anl.gov/AR/otter/examples33/program/two_inv.in> にあるので、実際に実行してみた。以下ネタバレ注意!!

• 実行ログ
• 証明から抽出した回路をGraphvizで適当に整形したPNG (.dot)

今だと25秒で解けているが、当時の486マシンで40分かかったそうで、大体100倍高速化した計算か。

Otterの入力ファイルをまじめに読んだのは初めてだったのだけど、Prologみたいに結構汚いことが出来るのね。$VARなんてPrologのvarメタ述語そのものじゃないか。そして、汚いけど、このリソースの扱い方は非常に巧妙で感心した。 記述する論理を線形一階述語論理にすれば、もっと素直に書けるだろうとも思うが、そういえば線形論理の定理証明機とかってあまり聞かないな。 線形一階述語論理に基づいた線形論理プログラミングよりも更に聞かないけど、なんでなんだろうね。

ついでに、Otterの後継のProver9でも試そうと思ったのだけど、Prover9はOtterよりも純粋な定理証明機のようで、同じテクニックは使えなさそうだった。うーむ。