トップ «前の日記(2008-07-16) 最新 次の日記(2008-07-19)» 月表示 編集

日々の流転


2008-07-18 [長年日記]

λ. Otter で 3 not problem を解く

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

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

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

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

本日のツッコミ(全2件) [ツッコミを入れる]
ψ なおえ (2008-07-28 12:40)

otterに後継があったなんて全く知らなかった<br>良い情報をありがとう!

ψ さかい (2008-08-01 00:43)

おお、なおえさん、Otter使ってたんですねー