2008-10-29 [長年日記]
λ. Seven Trees 問題を定理自動証明器を使って解く
Seven Trees 問題を解くときに、一階述語論理の定理自動証明器を使って解けないか試していた。 そのためには、以下の等式を公理として、T = T7 を証明させれば良い。
- x+y = y+x
- x+(y+z) = (x+y)+z
- x×y = y×x
- x×(y×z) = (x×y)×z
- x×(y+z) = (x×y)+(x×z)
- 1×x = x
- T = 1+T×T
最初にSPASSで試したのが 7trees.dfg だけど、これは止まらなかった。 可換性と結合性を直接サポートしていないのが不味いのではないかと思い、The E Equational Theorem Prover で試してみたのが 7trees.lop で、これもやっぱり止まらなかった。 あと、EQPなんかも試してみたが、これは使い方がいまいち良くわからなかった*1。
ここで諦めて結局手で解いてしまったのだけど、ふと思いついて以下のような公理(を途中で打ち切ったもの)から T1 = T7 を証明させてみたところ、うまくいった。
- x+y = y+x
- x+(y+z) = (x+y)+z
- T1 = T0+T2
- T2 = T1+T3
- …
これはいわば全て展開した多項式だけを対象にすることにしたもの。 ここで Tk+1 = Tk + Tk+2 は最初の公理系の定理なので、Tk を Tk で解釈すれば、この公理系における証明から最初の公理系における証明が得られる*2。 で、実行してみたところ、SPASSでもEでも一瞬で証明できた。 出てきた証明は、「Seven Trees やっと解けた」で手で導出したものと、ほぼ同じもの。
人の目から見るとどっちの公理系も同じようなものだけど、ちょっと工夫して問題を変形してやるだけで自動定理証明には劇的な効果がある、というのが面白かった。
【2009-02-15追記】 さらに、他の定理証明器として Prover9 と Equinox でも試してみた。
- Prover9は既に試した定理証明器と同じく、元の問題7trees.inは止まらず、単純化した問題7trees2.inは一瞬で解けた。
- Equinoxは残念ながら元の問題7trees.tptpでも単純化した問題7trees2.tptpでも止まらなかった。
λ. 水泳1km
今日も帰りに1km泳いできた。 かかる時間はちょっとずつ短くなって、今日は1kmで25分くらい。
λ. 【金融危機】日銀、利下げも検討 急激な円高・株安を懸念
「金融緩和を検討する」と言いつつ、実際には「日銀は独自の施策として、金融機関が日銀に預けている当座預金に利子を付ける方針」という、まるで正反対のことをしてるのね。 意味不明すぎる。 これが日銀クオリティwww
