ヨシ、CからBを作った。AとBからXが作れるな。ヨシ、AとBからXを作った。この方法だと、CやBをいじっているときに、必ずしもXが作れると確信してないかも知れません。最初に、DやEをゴニョゴニョしていて、Xを作れないかも知れません。DやEからXとは別なYが作れた、なんて事もあります。フォワード・リーズニングだと、作業のはじめの段階で何から手を付けていいかはよく分からないのです。作業工程も試行錯誤が入る発見的なものになるでしょう。ソフトウェアによる支援(次に何をすべきかのアドバイスとか)は、やりにくいでしょう。人間は、目的から逆向きにたどるバックワード・リーズニングだけで証明(やその他のこと)をやっているわけではありません。フォワード・リーズニングとバックワード・リーズニングを、けっこう複雑に混ぜて使っているのです。バックワード・リーズニングしか使うな、と言われると途方に暮れたりツラい気持ちになります。フォワード・リーズニングの対話的サポート現存の証明支援系で、フォワード・リーズニングに基づく証明が一切書けないわけではありません。書けるのですが、一人で/自分だけでエディタでモクモク・ツラツラと書きくだすだけです。バックワード・リーズニングのときのように、ソフトウェアと一緒に作業する環境ではありません。ツラい、寂しい、つまらない。あるので、ソフトウェアが介入・支援する余地はあると思います。証明支援系がフォワード・リーズニングをまったく手伝う気がないのは、歴史的惰性にすぎないかも知れません。やればできる子なのに、習慣で何もやらない、と。「愚痴と文句」を言ってみても、どうこうなるとは期待してませんが、仮にソフトウェア実装が出現しなくても、フォワード・リーズニングの対話的コマンド(いわば、逆タクティク)がどうあるべきかを考えるのは有意義だと思います。証明」のはずだがカリー/ハワード/ランベック対応の話を何度かしました。1はてなブログをはじめよう!m-hiyamaさんは、はてなブログを使っています。ブログを報告する引用をストックしましたストック一覧を見る閉じる引用するにはまずログインしてくださいログイン閉じる引用をストックできませんでした。再度お試しください閉じる限定公開記事のため引用できません。