aboutme:137129
定理証明器を使っている感覚、つまり、形式性をつきつめた感覚では「対角線論法」というのは使ってるようには思えなかった。並べて「見る」以上、それは人の感覚器を通じている。定理証明器上では、(二重)否定を含む命題を帰納法でどう解くかとしか感じられないのではないか？
JRF 2011年2月26日 (土)
(半)自動証明付きの定理証明器では、人の証明テクニックを使わないほうが、自動証明には有利であることがあった。
例えば、計算論の専門分野になるが、ラムダ計算の Church-Rosser 性を示すのに、「平行導出(pararell reduction)」という証明テクニックは必要なかったというような結果を読んだことがある。
JRF 2011年02月26日 0017
形式性をつきつめた感覚も感覚器を通じるわけだが、「見る」ことをフィードバックするなどの人の感覚器に備わる証明器的機能は使わない。理性だけで相互作用して脳だけに蓄積される特殊な制御かつ従属の感覚といったらいいのか…。(「それが第六感」とはとうていいえないが、体内のことだけでもやっぱりそれも感覚だろう。)
JRF 2011年02月26日 6761
あと、逆に、「感覚的な証明」、例えば、ラムダ項を樹形図に描いて、その位置的つながりに関して証明の説明をする…なんてのは人間にはわかりやすいが、証明として本当に rigid (厳格)なものか他者が確認しようがなかった。が、その「直感的な説明」を長々と入力しさえすれば、本当に証明になっているかをコンピュータが厳格に確認してくれるということはできた。(…というのが私の修論(博士課程前期修了のための論文)の主旨だった。)
JRF 2011年02月26日 0788
(あれ理科系の国際的な基準で「論文」って言っていいのかな？指導教官以外の普通の意味での査読者は実質いないんだけど…分量の多いレポートぐらいの扱いになるのでは？内容も要するにそういう例を一つ出したというだけで、新規性を主張するわけでもないのに、一般性のある成果になってないし。)
JRF 2011年02月28日 3190
(↑の論文うんぬんは↓のニュースを意識している。ちなみに理工系の実情を考えると、↓の方向は負担を増やすだけのように思う。5年か6年で博士号をとろうとする「論文が書ける人」は、前期(or 修士課程)で国際的に通用するような論文を１本は書ける成果を出してないとダメだろうし、そうでない人も、命じられた作業が忙しかったりするので、他の分野のことをやってる暇はないと思う。)
《中央教育審議会、大学院博士課程の改革を提言。「徒弟制度」や、修士論文の廃止などを求める - スラッシュドット・ジャパン》
http://slashdot.jp/article.pl?sid=11/02/01/0742253
JRF 2011年03月03日 9347
トラックバック
他サイトなどからこの記事に自薦された関連記事（トラックバック）の一覧です。
結城浩『数学ガール ゲーデルの不完全性定理』を読んだ。おもしろい。私のかつての専門分野だが、私の不完全性定理の理解は不完全なものだったのだな、と気付かされた。 続きを読む
受信： 2017-09-30 06:55:08 (JST)
いや、ちょっとその分野から離れてるんで、今そういうテクニックとして「対角線論法」なる半自動証明戦略があったりするかもしれないけど。
…うーん、これも私が確かめるべきだな…。今やってることが一段落したら、リハビリに今の定理証明器で簡単な理論の証明演習をやってみるかな。
JRF 2011年02月26日 5654