13/10/08 20:22:13.24 .net
>>214
それが可能ならそれこそ形式仕様なぞ不要だな
そもそも何でも証明器で検証するのが前提になってる>>206は
形式手法にどんな夢を見ているんだ？
>>206
> 放っておいても証明器は完璧にそうしてくれる。
> 同じことを君（人間）がやってもそれこそ効果は半減する。
残念ながら証明器は放っておいても何もしてくれない。
証明器を有効に使うために必要なエフォートを知った上での
主張とは思えない。
> どんな相手だろうと、何を書いて
> いるかを伝えるためには、単なる記号では伝わらないんだよ。
piを「円周率」として読むレベルの厳密さで良いのであれば、
拘束文法による半形式仕様で十分だ。