トップ «前の日記(2011-11-10) 最新 次の日記(2011-12-28)» 月表示 編集

日々の流転


2011-11-18 [長年日記]

λ. TPP2011のTPPmarkをZ3で解いてみた

昨日・今日で定理証明のイベント 7th TPP (2011) が開催されている。 私は残念ながら参加できないのだけど、お題(TPPmark)「Uniform Candy Distribution」 をSMTソルバZ3で解いてみた。

Z3等のSMTソルバは、通常の自動定理証明器や対話的定理証明と比べ、全称量化子や帰納法の取り扱いに制限があるため、その辺りでは苦労したものの、この程度の補助でこれだけ証明できるなら結構使えると感じた。

問題ページで、集まった解答が公開されているが、それを見ると私以外はIsabelle/HOLとCoq(+SSReflect)しか使ってなくて、他のツールの使い手は不甲斐ないなぁと思った。 ACL, PVS, Mizer あたりがいないのは参加者層が偏ってそうだ。 あと、汎用の定理証明ツールではないけど、MaudeやCafeOBJとかでどう扱われるのかとかも見てみたかったかも。