コンピューターによる定理の自動証明at MATHコンピューターによる定理の自動証明 - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト500:１３２人目の素数さん 09/01/18 11:20:15 ちなみにピタゴラスの定理だとCで何行ぐらいになるの？ だいたいでいいんだけどさ。 500行ぐらい？ それとも100億行ぐらい？ 501:１３２人目の素数さん 09/01/18 11:22:59 証明を見つけるプログラムってprintfで表示するの？ 日本語で？ 502:１３２人目の素数さん 09/01/18 12:41:55 計算機での自動証明の話で、 ヒルベルトのプログラムだのゲーテル数だのを持ち出す方が よっぽどバカだと思うのだが．．．。 そういう無茶な風呂敷の広げ方をするから、 一般人は>>500のような反応をするわけで。 実際に自動証明の研究でやっていることはといえば、特定の分野で 限られた定理の組合せで証明できる範囲に限定して、 前提となる事実・帰結・推論規則としての定理・定理を適用する上でのノウハウ 等を、その範囲に限定して設計された記述言語で記述しておいて、 それらを利用して、人間には比較的簡単に行えるような証明を構築するプロセスを 計算機にトレースさせるというような試み。 つまり、人間にできないような証明を計算機にやらせるなんてことを いきなり目指してるのではなく、まずは人間の思考というものを プログラムでモデル化してみることで、人間的な有機的な物事の捉え方を 計算機で応用するための知見が得られないかを探る基礎的な研究であって 本質的には人間工学に近い分野。あとはノレッジベースとかＡＩ（死語）とか。 実際に素材としている数学の分野は、簡単な定理の組合せで証明できる 初等幾何が主流。それも、ピタゴラスの定理のように数値の計算が からむようなものは「簡単な定理」の範囲に入らない。 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch