2010-07-04 [長年日記]
λ. 「掛け算から足し算を作る」を定理証明器で
檜山さんの「掛け算から足し算を作る（パズルとしてやってみよう）」の証明の部分を定理証明器に証明させてみようとしてみた……がうまくいかず。
SPASS で試してみたのが AGS.dfg で、The E Equational Theorem Prover(eprover) で試してみたのが AGS.tptp 。 どちらの場合でも、conjectureを一個ずつ試したところ、x+0=x と加算に関する逆元の存在はすぐに証明できるのだけど、他は組み合わせ爆発している感じ。 適当に補題を追加すればいいかと思ったけど、それでもそもそも公理の数が多いとダメみたい。 ……残念無念。
[ツッコミを入れる]
