コンピューターによる定理の自動証明
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/06(火) 23:35:120449１３２人目の素数さん
2009/01/13(火) 00:08:35計算機での証明を行う場合も、四捨五入なんかする必要はない
>>446のように何らかの代数的性質を満たす記号として √ を導入すればいいだけ
√x と √y の大小関係もその代数的性質から証明できる話。
>>448のやり方がそのひとつだな
まあ、コンピュータによる完全な自動証明は無理だが、
人間がやる証明の支援くらいは出来るようになるかもしれないとは思っている
0450１３２人目の素数さん
2009/01/13(火) 00:12:51一応コンピュータでの証明支援は既にあることはある。
0451１３２人目の素数さん
2009/01/13(火) 11:11:080452１３２人目の素数さん
2009/01/14(水) 10:26:500453１３２人目の素数さん
2009/01/14(水) 10:58:01ver4から3次元曲面がマウスでぐりぐりできるようになったよね。
0454１３２人目の素数さん
2009/01/14(水) 12:32:490455１３２人目の素数さん
2009/01/15(木) 10:05:39あらゆる実数に関する命題は
具体的数値（1,2,3,4,5,6,7,8,9,0）を全く使用せず
抽象的数値（a,b,cなど）で全て証明することができる。
という定理があるということか？
0456１３２人目の素数さん
2009/01/15(木) 10:09:400457１３２人目の素数さん
2009/01/15(木) 10:28:410458１３２人目の素数さん
2009/01/15(木) 10:30:090459１３２人目の素数さん
2009/01/15(木) 10:58:22長々と説明なんてしなくていい
そういう定理が「ある」か「ない」か
2文字で済む話じゃないか。
0460１３２人目の素数さん
2009/01/15(木) 12:47:08√2を小数で表した物が具体的数値で√2が抽象的数値だって？
誰の脳内設定だよ 実数の構成も理解して無いだろ
0461１３２人目の素数さん
2009/01/15(木) 13:12:280462１３２人目の素数さん
2009/01/15(木) 14:36:30＞そういう定理が「ある」か「ない」か
に答えてもらえば解決すると思ってんだからなあ。マナカナのどっちが美人かを決めれば
解決すると思い込むのと変わらんよなあ。
結局、バカは自分がバカだと認識することはできないんだなあ。
0463１３２人目の素数さん
2009/01/15(木) 15:05:45晒しあげ
0464１３２人目の素数さん
2009/01/15(木) 15:12:310465１３２人目の素数さん
2009/01/15(木) 16:51:59そんな長い文章はいらない。2文字でいい。
>>464
実数に関する証明はあらゆるをつけなければ意味がない。
たった２，３個の実数で成り立った所で何の意味もない。
∀a∈Rについて成り立たなければそれは実数における定理の資格はない。
抽象的な文字（a,b,c・・・）で解決できるから
具体的な数値など求める必要はないと言ったのはそっちだ。
そういう定理がなければそんな発言は出てくるはずがないからな。
0466１３２人目の素数さん
2009/01/15(木) 16:53:40どっちが晒しあげられてるかも気付かないのね・・・
0467１３２人目の素数さん
2009/01/15(木) 16:59:32「ない」
というか具体的数値とやらを使用しようがしまいが
あらゆる実数に関する命題を全て証明することはできない
0468１３２人目の素数さん
2009/01/15(木) 17:02:32晒しあげ
0469１３２人目の素数さん
2009/01/15(木) 17:03:530470１３２人目の素数さん
2009/01/15(木) 17:07:27Mathematicaで「√3＞√2」を評価したとき
それぞれを小数展開してそれらの各桁を比べてるとでもと思ってるの？
0471１３２人目の素数さん
2009/01/15(木) 17:19:29ではでは。
0472１３２人目の素数さん
2009/01/15(木) 17:22:160473１３２人目の素数さん
2009/01/15(木) 17:24:28＞あらゆる実数に関する命題は
は
あらゆる実数に関する「証明済みの」命題は
ってことね。
0474１３２人目の素数さん
2009/01/15(木) 17:27:01本当に知りたいなら付き合う気はあるけど
言葉遊びがしたいだけなら流石にやる気は無いぞ
0475１３２人目の素数さん
2009/01/15(木) 17:43:110476１３２人目の素数さん
2009/01/15(木) 17:53:34超数学的なことをせずスピードを問わないのならどうとでもなる
0477１３２人目の素数さん
2009/01/15(木) 20:25:350478１３２人目の素数さん
2009/01/16(金) 01:51:07真実追求しかしていない。
抽象的数値a,bには大小関係が定義されていない。
aとbどっちが大きいか？という問いに意味がない。
アルファベットに大きいも小さいもないからな。
a、bに具体的数値を代入して初めて大小関係が定まる。
ところが、ここの住人は具体的数値を求める必要はないと言う。
じゃあ質問するがaとbはどっちが大きい？
ただしaとbには具体的数値は代入されていないものとする。
ただ、おれは>>448で大小関係はプログラムで求められることに気づき
その部分においてのみ、自らのあやまちは認めたはずだ。
0479１３２人目の素数さん
2009/01/16(金) 02:27:10晒しあげ
0480１３２人目の素数さん
2009/01/16(金) 06:17:04どのレスだよ
0481１３２人目の素数さん
2009/01/16(金) 12:16:160482１３２人目の素数さん
2009/01/16(金) 19:26:59a^2=xを満たす正の実数aと、b^2=yを満たす正の実数bがともに存在するとしよう。
このとき、a≧bと仮定すると、x=a^2≧b^2=yとなり矛盾する。
従ってそのようなa,bが存在すれば、a＜bである。
0483１３２人目の素数さん
2009/01/16(金) 22:13:330484１３２人目の素数さん
2009/01/17(土) 02:27:00この時点でダメだな。
単なる文字に大小関係は無いの。
ｘ＜ｙとする
なんてやってるということはｘとｙにはなんらかの実数、
つまり具体的数値が代入されていることを予定しているんだろ？
アルファベットに大小関係は無いの。
もうほっとこう。だめだ。
0485１３２人目の素数さん
2009/01/17(土) 02:42:12（´,_ゝ｀）ﾌﾟｯ
0486１３２人目の素数さん
2009/01/17(土) 03:18:41吠えてるスレはここですか？
0487１３２人目の素数さん
2009/01/17(土) 07:58:27晒しあげ
0488１３２人目の素数さん
2009/01/17(土) 21:16:41内燃機関を発明できるか？
どういう構造にしたら効率がよいか、とかは得意だろうけど
仮にできたとして、
内燃機関を発明するアルゴリズムは、内燃機関を知っている何かでなければ構築できないのではないか？
0489１３２人目の素数さん
2009/01/17(土) 22:05:18実際に打つ前にフローチャート書く。
（フローチャートを書かなくても、図とか絵とか描いて矢印書いたりして
なんらかのフローチャートもどきは書く）
ならそのフローチャートが証明になっちゃってるじゃん。
0490１３２人目の素数さん
2009/01/17(土) 22:33:28自動証明ってのは、プログラムを生成するプログラムを書くような
ものなんだよ。
0491１３２人目の素数さん
2009/01/17(土) 23:36:28そのプログラムはフローチャートでは表すことは出来ないの？
0492１３２人目の素数さん
2009/01/17(土) 23:48:14知ってていってんだろうな。
つーか。ゲーデル数化も何もしらなそうだな。
0493１３２人目の素数さん
2009/01/17(土) 23:51:30↑教えてください！
0494１３２人目の素数さん
2009/01/17(土) 23:53:40アルゴリズムって言うとき、自分の感覚では、証明出来るなら証明し、出来ないなら出来ないと有限ステップでわかるようなものってイメージなんだけど。
0495１３２人目の素数さん
2009/01/18(日) 00:09:54マルチ
0496１３２人目の素数さん
2009/01/18(日) 03:16:45その定理が真であることを求めるプログラムをCでも何でもいいんで
書いてもらえませんか？
ピタゴラスの定理でもいいですよ。
0497１３２人目の素数さん
2009/01/18(日) 10:41:50いやいや、すまんかった。結局こういうやつ>>496がいるからさあ。ちったあ入門くらい自分でやれ
と言いたくなる。
0498492=497
2009/01/18(日) 10:46:57少しはヒント出すか。１，２，３，．．．と自然数を順に調べていけば、その中にピタゴラスの定理の証明が
あるんだけど。意味わかんねーだろ。だから、ゲーデル数化ぐらい知っとけっての。
あ、それから、真であることを求めるプログラムじゃなくて、証明を見つけるプログラムな。
真と証明可能の違いくらいも早く知っとけ。
0499１３２人目の素数さん
2009/01/18(日) 11:18:47うん、わかんね。
真と証明可能の違いはわかる。
真だからといって証明可能かどうかは保障されてないもんな。
でも証明可能なら真ってことだ。
0500１３２人目の素数さん
2009/01/18(日) 11:20:15だいたいでいいんだけどさ。
500行ぐらい？
それとも100億行ぐらい？
0501１３２人目の素数さん
2009/01/18(日) 11:22:59日本語で？
0502１３２人目の素数さん
2009/01/18(日) 12:41:55ヒルベルトのプログラムだのゲーテル数だのを持ち出す方が
よっぽどバカだと思うのだが．．．。
そういう無茶な風呂敷の広げ方をするから、
一般人は>>500のような反応をするわけで。
実際に自動証明の研究でやっていることはといえば、特定の分野で
限られた定理の組合せで証明できる範囲に限定して、
前提となる事実・帰結・推論規則としての定理・定理を適用する上でのノウハウ
等を、その範囲に限定して設計された記述言語で記述しておいて、
それらを利用して、人間には比較的簡単に行えるような証明を構築するプロセスを
計算機にトレースさせるというような試み。
つまり、人間にできないような証明を計算機にやらせるなんてことを
いきなり目指してるのではなく、まずは人間の思考というものを
プログラムでモデル化してみることで、人間的な有機的な物事の捉え方を
計算機で応用するための知見が得られないかを探る基礎的な研究であって
本質的には人間工学に近い分野。あとはノレッジベースとかＡＩ（死語）とか。
実際に素材としている数学の分野は、簡単な定理の組合せで証明できる
初等幾何が主流。それも、ピタゴラスの定理のように数値の計算が
からむようなものは「簡単な定理」の範囲に入らない。
0503１３２人目の素数さん
2009/01/18(日) 16:46:54ゲーテル持ち出しても何の意味もない
0504１３２人目の素数さん
2009/01/18(日) 17:20:16有限ステップでは証明できないが、証明可能な命題ってあるの？
0505１３２人目の素数さん
2009/01/18(日) 20:43:140506498
2009/01/18(日) 21:48:08をを！すまんかった。今は反省している。どうも>>498を読んだときバカにされた気が
して感情的になってしまったようだ。
おわびに、ゲーデル数化をしても、定理の自動証明にはあまり実用的でないということ
を例えで説明しよう。まず、使用する文字を決める。例えば、ひらがな全てでも良い。
カタカナを含めてもよい。いずれにしても使う文字は有限個に決める。例えばN個だと
しよう。文字を2つだけ並べた文字列は有限個しかない。今の例ならN×N個だ。文字を
3つだけ並べた文字列も有限個。4つ並べても有限個。．．．と行くと、いずれは例えば
ふるいけやかわずとびこむみずのおと
というような文字列も現れるし、ピタゴラスの定理の証明として読める文章も現れる。
それに、以上の手続きは簡単なアルゴリズムで書ける。もっと詳しく論理式とか、証明
を定義すれば、任意の文字列に対して、それが何らかの定理の証明になっているかを
判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
あるかどうかの判定をするアルゴリズムも書ける。
0507498
2009/01/18(日) 21:49:45だからといって、以上の方法が実用的でないということは容易にわかると思う。現在の
コンピューターでは演算速度も記憶容量も足りなすぎる。もちろんいずれ以上のような
方法でも十分実用になるような性能を持ったコンピューターが現れる日が来るかもしれ
ないが、そのころにはの方法で、もっと効率よく定理を証明するアルゴリズムが開発さ
れているかもしれない。
長文すまんかった。失礼。
0508498
2009/01/18(日) 21:52:04実用的でないということ。
0509１３２人目の素数さん
2009/01/19(月) 02:29:07なるほど。その発想はなかったわ。
行間を読む行為もしなくて済むだろうし。
要するに定理の証明とは「有限個の文字の羅列」なんだね。
でも、ここで数学をかじってる人間はすぐに一般化したくなると思うんだ。
「無限個の文字の羅列」で表される定理の証明はあるんだろうかとか
「文字と文字の間にじつはさらに文字があるみたいな、実数の稠密性みたいな文字集合」とか。
ところで
数学の定理は有限個の文字で証明できる
という定理はあるの？
0510１３２人目の素数さん
2009/01/19(月) 02:32:060511１３２人目の素数さん
2009/01/19(月) 02:33:510512１３２人目の素数さん
2009/01/19(月) 03:03:500513１３２人目の素数さん
2009/01/19(月) 11:10:46文字数が確定していないんだから
文章の数は無限個だから証明の文章はできないんじゃないの？
ある定理は100文字で証明終わりになるとはじめからわかっているなら
100個の文字のあらゆる組み合わせを調べつくせば済むけど
その定理の証明が100文字で終わることをどうやって事前に知るの？
0514１３２人目の素数さん
2009/01/19(月) 11:11:49>>498が話してるような方面の基礎論は関係なしで
0515１３２人目の素数さん
2009/01/19(月) 11:26:46あ.いうえおか
か.なにぬね
こういう文字集合を定義したら
証明できる命題は増えるんでしょうか？
0516１３２人目の素数さん
2009/01/19(月) 12:09:49ω規則ってどんなのですか？
0517１３２人目の素数さん
2009/01/19(月) 12:57:53科学が信仰する事実そのものという観念は、宗教、特にキリスト教の神観念に近い。
これは科学が西洋社会を起源にもつ文化現象であるという一つの証拠である。
キリスト教の神観念は、人間の外にある絶対者であり、人間にとって認識不可能かつ到達不可能な存在である。
これは正しく科学が前提とする事実そのものの存在と同じである。
ちみなに、仏教では一切の存在に仏の生命が宿ると考える。
仏性=真理は外にある絶対のものではなく、個々の存在に宿る内面的なものである。
真理は自身のうちにあり、外にはないと考える。
科学は真理を人間の意識の外に求めようとする点において、極めてキリスト教的、西洋的である。
到達不可能な絶対者を立てる科学は、キリスト教と同型の思考形態をもつ。
真理そのものがはなから自己のうちに宿ると考える仏教的発想によって、科学は相対化されるのである。
また、構造構成主義もシステム論も、意識から隔絶した事実そのものを定立することなく、世界を記述するので、科学とは観察方法が根本的に異なることになる。
0518１３２人目の素数さん
2009/01/19(月) 17:34:350519１３２人目の素数さん
2009/01/19(月) 18:18:180520１３２人目の素数さん
2009/01/20(火) 02:29:24文字に大小関係を導入したとたんに逃げるか。
おれだよ、おれ。
文字に連続性を持たせたとたんに口を閉ざすか。
もっとさらし上げろよ。
0521１３２人目の素数さん
2009/01/20(火) 10:45:360522１３２人目の素数さん
2009/01/22(木) 03:03:35だから使う文字を有限個にしたところで
出来上がる文章は無限個だろ。
そんなロジックもわからないのか。
あ
ああああ
ああああああああ
ああああああああああああああ
わかるよな？
あだけで無限個文章があるよな？
まさか逃げはしないよな？
0523１３２人目の素数さん
2009/01/22(木) 04:04:150524１３２人目の素数さん
2009/01/22(木) 20:00:18グッドスタインの定理を途中に出てくる式全部きっちり計算して証明すればいいし
チャイティンの定数も十進表記で計算し終わってから議論すればいい
0525１３２人目の素数さん
2009/01/23(金) 02:11:290526１３２人目の素数さん
2009/01/23(金) 05:55:360527１３２人目の素数さん
2009/01/23(金) 14:16:25晒しあげ
0528１３２人目の素数さん
2009/01/24(土) 01:52:30よく戻ってきたな。
じゃあ話を聞かせてくれ。
ゆっくりでいいぞ。
緊張しなくていいんだぞ。
0529１３２人目の素数さん
2009/01/24(土) 05:05:11晒しあげ
0530１３２人目の素数さん
2009/01/24(土) 09:49:08,,==≡ミヽミヾミミミ、ヾ、
_=≡≡三ミミﾐ ミﾐヾ、ソ)),,》 .
彡彡二二三≡ミ-_ ﾐﾐ|ノﾉj )||ヽ, )、
__,,,,,,,,,／彡二二二 ,- __ﾐ|/ﾉ ﾉﾉﾉﾉ) ||
-=二ミミミミ----==--'彡 ∠ミﾐ_ソノノノﾉ ﾉ
/／＞=''"二二=-'"_／ ノ''''')λ彡／
,,/￣''l 彡/-'''""￣-=彡彡／ ,,-''",,,,,,,ノ .彡''"
(, ,--( 彡 ,,-- ===彡彡彡"_,-＿ ヽ Υ
ヾ-( r'''''＼ ／／=二二''''''彡ｿ￣ ∠__＼ .＼ｿ .|
＼;;;; ＼ Ζ彡≡彡-'''',r-､> l_"t。ﾐ＼ﾉ,,r-v ／￣￣￣￣￣￣
＼;;;; ＼ 彡""彡彡-//ヽ" ''''''""￣'''""(ｴｱ/ ／
＼;; ＼'''''')彡ヽ// | (tv ／| , r_>'| ＜一体みんな誰と戦っているんだ
＼;;; ＼'" ＼ ,,"''-,,ﾉ,r-", / r'''-, .j ＼
＼;;; ＼ ／,,>--'''二"''' r-| 二'" / __ ＼＿＿＿＿＿＿
＼;;r'""彡_l:::::::::::::::::::::: /./_ " ／￣￣"===-,
)''／／rl_--::::::::::::::::/:/ヽ"'=--":
0531１３２人目の素数さん
2009/01/26(月) 09:39:21>判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
>あるかどうかの判定をするアルゴリズムも書ける。
ええ、うそでしょ？
ならそのアルゴリズムがすでに定理の証明になっちゃってるじゃん。
0532１３２人目の素数さん
2009/01/26(月) 12:00:37を使えば、ある文字列(式)がどのような定理(型)を証明しているか、それとも間違っている(型エラー)か自動判定することができる。
しかし、逆に、定理(型)からその証明(式)を導くことは完全自動では無理。
0533１３２人目の素数さん
2009/01/26(月) 14:35:49問題を入力すると、その問題を２ちゃんやYahoo!やOKWaveとかの質問スレに自動的に書き込んで、結果を読み込んで戻ってくる。
そういう掲示板だけでなく、あらかじめ指定したアドレスへ質問メールを出して、返答を受けることも可能。
これで殆ど解決。
でも最近、回答の精度が落ちてるんだよなあ。「マルチポストはヤメレ」「質問ばかりするな」なんていう意味のない回答が良く来るようになった。
どうしてこうなったんだろう。プログラムのミスかなあ。
この辺をどう解決するかが今後の課題。
0534１３２人目の素数さん
2009/01/26(月) 17:47:35虱潰せばできるけどね
簡単な定理でも地球が滅びるくらいの時間が掛かるだろうけど
0535１３２人目の素数さん
2009/01/26(月) 19:46:43それは反則ではないのか？
0536KingGold ◆3waIkAJWrg
2009/01/27(火) 18:05:140537１３２人目の素数さん
2009/01/27(火) 23:14:04証明はDNAパソコンでしょ
0538１３２人目の素数さん
2009/01/27(火) 23:16:47そういうソフトはすでに存在しているんじゃね？
オープンにされてないだけで。
簡単につくれるし。
0539１３２人目の素数さん
2009/01/27(火) 23:26:430540１３２人目の素数さん
2009/02/06(金) 10:13:49プログラムによって解かせるものを考えた。
でもこれって既出かな？？？
0541１３２人目の素数さん
2009/02/07(土) 08:19:23ソースきぼんぬ
0542１３２人目の素数さん
2009/02/07(土) 10:07:420543１３２人目の素数さん
2009/02/07(土) 10:14:34ネタの仕込みからにぎりまで
そばロボットもいい
0544540
2009/02/07(土) 10:29:02『数学的帰納法』で
１．等式の証明
２．不等式の証明
があるけど
正の整数（自然数）のみ動かせば
負の整数の場合も自動的に掃きだしてくれる。
0545１３２人目の素数さん
2009/02/11(水) 08:53:40の証明を
P(0) かつ \forall k \in N, (P(k) => P(k+1))
を使って自動証明するってことだよね。
具体的にどんなことが自動でできるの？kwsk
0546１３２人目の素数さん
2009/02/11(水) 17:31:47論理的に式変形をしてしらみつぶしに解いていくだけ
0547１３２人目の素数さん
2009/02/11(水) 23:16:09とかも自動証明できたりする？
0548１３２人目の素数さん
2009/02/12(木) 11:49:28ぜひどうなるか知りたいね。
■ このスレッドは過去ログ倉庫に格納されています