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とかでどう扱われるのかとかも見てみたかったかも。
[ツッコミを入れる]
