コンピューターによる定理の自動証明
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/06(火) 23:35:120602１３２人目の素数さん
2009/03/07(土) 13:11:32座布団一枚
0603１３２人目の素数さん
2009/03/09(月) 16:10:20うん、それ無理。
ペアノの公理系で、加法の交換法則は定義されてるの。
この公理をペアノの公理系の内部で定理として証明するのは
不可能だったはずよ。
0604１３２人目の素数さん
2009/03/09(月) 22:01:170605１３２人目の素数さん
2009/03/10(火) 01:18:03> >>549
> うん、それ無理。
>
> ペアノの公理系で、加法の交換法則は定義されてるの。
> この公理をペアノの公理系の内部で定理として証明するのは
> 不可能だったはずよ。
ゴルァ、シレっとウソつくんじゃねえｗｗｗｗｗ
『ペアノ数の概念について』（小野勝次・梅沢敏郎 訳・解説）、共立出版
のp.111に９という番号の付けられた
a, bεN . ⊃ . a+b=b+a
って式が定理として挙げられてるぞ。ペアノ自身の証明はそれを見ろ。
0606１３２人目の素数さん
2009/04/05(日) 16:11:55脳は分子機械に過ぎないのだから
証明は心霊現象になってしまう
0607１３２人目の素数さん
2009/04/08(水) 20:10:51http://ja.wikipedia.org/wiki/%E8%87%AA%E5%8B%95%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E
にでてる「ハーブランド賞」てエルブランじゃね？
0608１３２人目の素数さん
2009/04/09(木) 05:28:18Herbrandの仏語の音をカタカナで近似すれば「エルブラン」、
英語読みした音をカタカナ書きすれば「ハーブランド」
0609１３２人目の素数さん
2009/04/26(日) 22:10:30Coqのバージョン8.2ではコンパイル出来ないんですが
なぜだかわかる方居ますか？
このPDFはかなり面白そうな感じがするんですが
実際に動かせないので悲しいです
別のバージョンだと動いたりするんでしょうか
Fixpoint tupleT (A:Type) (n:nat) : Type :=
match n with
| O => unit
| S m => A * tupleT A m
end.
全般的に依存型に関する情報が少ないもので困ってます
0610１３２人目の素数さん
2009/05/03(日) 08:30:48Open Scope type_scope.
の１行を最初に書くと私の環境ではコンパイルとおりました。
Coq 8.1pl2 と8.2 でコンパイルが通ったことを確認しました。
0611１３２人目の素数さん
2009/05/03(日) 11:27:41ベジータ「数学は科学基礎だ!!
舐めるなよー!!!!｣
>>595
宇宙→銀河系→太陽系→惑星→分子→原子→素粒子→クォーク→…
無限階層説があるのう｡
0612１３２人目の素数さん
2009/05/05(火) 00:30:01動きました!
諦めかけてたのですが、ありがとうございます!
0613１３２人目の素数さん
2009/07/08(水) 17:10:040614↑
2009/08/11(火) 21:15:590615１３２人目の素数さん
2009/08/15(土) 13:26:46定理証明支援系と依存型プログラミング勉強会
ttp://tzik.homeunix.net/ap2007/wiki/index.php?%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E%E6%94%AF%E6%8F%B4%E7%B3%BB%E3%81%A8%E4%BE%9D%E5%AD%98%E5%9E%8B%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%9F%E3%83%B3%E3%82%B0%E5%8B%89%E5%BC%B7%E4%BC%9As
0616１３２人目の素数さん
2009/08/15(土) 17:37:17> コンピューターによる定理の自動証明
> これが可能になったら数学者という仕事が無くなっちゃうの？
1 にマジレスすると、自動証明できる空間は非常に小さくて、ほとんど意味が無い。ということが証明されている。
むしろ多くのひとが興味のあるような命題は機械の支援に加え人間の手が必ず必要になる。
これは普通の数学だとあんまりうれしくない事実だけど、コンピュータの動作の保証が得られることは、プログラムの世界では
非常に重宝される技術。例えば、原子力施設のプログラムや、鉄道や道路の信号のシステム、医療、金融関係のシステムは不具合が許されない。
結論を言うと、定理証明の技術が発展すれば、数学者はプログラムの基幹システムにおいて、むしろ必要不可欠になる。
だから、数学者はプログラム技術を、プログラマは数学をしっかり学んでおくと将来お徳だと思う。
以上が私の妄想。
0617１３２人目の素数さん
2009/08/21(金) 22:58:470618１３２人目の素数さん
2009/08/22(土) 11:03:50実数の集合は有理数の集合より大きい濃度を持つ
0619１３２人目の素数さん
2009/09/07(月) 00:35:120620１３２人目の素数さん
2009/10/13(火) 21:35:41よくある論理パズル（正直者と嘘つきがいて、ある人が〜と言った。とかいうやつ）を
coqで解きたいと思ったのですが
要するに命題論理の式をCNF(乗法標準形？）に変形できればいいのですが
coqでうまくやる方法をご存知の方いますか？
0621sage
2009/10/15(木) 16:29:240622sage
2009/10/15(木) 16:31:570623１３２人目の素数さん
2009/10/16(金) 00:37:23元の質問の動機は、スマリヤンの本の序盤のパズルを
覚えたてのcoqを電卓がわりに使って解けないかというぐらいのものなので、
ちょっと問題が大きい感じです。
hnfというtacticが標準であるので、
他の標準形にもちょいちょいと直せないものかと思った次第です。
0625１３２人目の素数さん
2009/10/16(金) 12:19:06Wikipediaにまとめがありました。
http://en.wikipedia.org/wiki/Knights_and_Knaves
日本語なら
http://www.kai.ed.jp/math/gakusyuu/2002minami.htm
というのが検索で出てきました。
よくあるパズルとか書きましたが、
スマリヤンがオリジナルなのかもしれません。
0626１３２人目の素数さん
2009/11/02(月) 13:37:580627１３２人目の素数さん
2009/11/03(火) 05:57:33どうも、「ＥＵＲＭＳ（∋ M_SHIRAISHI氏 ）の理論」のほうが正しいようだな。
例えば、《仮言三段論法の原理》は、従来は、 [(Ｐ⊃Ｑ)＆(Ｑ⊃Ｒ)]⊃(Ｐ⊃Ｒ) で
表わされるもののことと考えられていたのだっただが、これは、どうやら、誤りだった
ようだ。
そして、ＥＵＲＭＳの言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)]＆[Ｑ(ｘ)⇒/x/Ｒ(ｘ)］⇒/p,q,r/［Ｐ(ｘ)⇒/x/Ｒ(ｘ)] 1{Ｑ」
こそが、《仮言三段論法の原理》を 正しく捉(とら)えてたものと考えられる。
ＥＵＲＭＳの主張する「論理＊大＊改革」は、恐らく、世界を席巻することとなろう。
http://www.age.ne.jp/x/eurms/RONRI-J02.html#E-Books
0628１３２人目の素数さん
2010/02/04(木) 17:16:300629１３２人目の素数さん
2010/03/02(火) 21:35:271年前のレスだが、1mがプランク長の整数倍じゃないのは誤差だから。
0630１３２人目の素数さん
2010/03/02(火) 22:19:16厳密な整数倍じゃないのは単なる誤差
0631１３２人目の素数さん
2010/03/02(火) 22:43:530632１３２人目の素数さん
2010/03/06(土) 01:03:580633１３２人目の素数さん
2010/03/06(土) 02:30:58それを言うならば、そもそも選択公理を用いた数学で物理理論を記述してるのがナンセンスなのだが
フルスペックの選択公理はBanach-Tarskiのパラドックスを導いてしまうからね
>>631
うん、例えばクーロンの定義が電気素量ｅの１Ｎ（アボガドロ数）倍（つまり１モルの陽子の電荷総量）なら明解なんだけどね
現在は電流単位としての１Ａ（アンペア）をその電流が流れる電線の間の力の強さで定義して
１Ａの強さの電流で１秒流れる電気量を１Ｃ（クーロン）として定義してるからなあ
質量の単位のｋｇについても今のキログラム原器なんて怪しげというか恐ろしく原始的な定義じゃなくて
炭素１２原子核の質量の１Ｎ倍を１２グラムとして定義しようというアイデアはかなり昔からあるんだよな
あるいは陽子（普通の軽い水素の原子核）の質量の１Ｎ倍を１ｇと定義すればもっと明解だな
炭素１２原子核にしろ陽子にしろ、そういうものの質量なら質量分析器を用いて極めて精密に測れるからね
今は逆にアボガドロ数の定義として１２ｇの炭素１２に含まれる炭素１２の原子数を用いていたんじゃないかな
（つまり上の新しい定義の提案だと、アボガドロ数は実験で決まる定数でなく最初から値を定めておく定数にせねばならない）
0634１３２人目の素数さん
2010/03/06(土) 23:28:1010進数は人間の指の数が起源だからある意味原始的。日常生活での16進数への移行は難しいが
0635１３２人目の素数さん
2010/03/09(火) 13:08:15数はどの底をとっても恣意的でしょう。
もっというなら16進数よりは2進数のほうが本質だと思う。
0636１３２人目の素数さん
2010/03/10(水) 22:09:120637１３２人目の素数さん
2010/03/15(月) 12:27:50のが本質。但しこれだと０を表すことができないので、
個数に１個げたを履かせることで回避するようなことをしなければ
ならない。
たとえば
０： ×
１： ××
２： ×××
１０： ×××××××××××
。。。。
0638１３２人目の素数さん
2010/03/16(火) 01:21:49底とかナシで無限個のシンボルをつかって表現するのが本質なんじゃない？
つまりどの数も違うひとつの記号で表されるって感じで。
実際は、これを実現するのが無意味に大変だから、
「わかりやすい」とか「つかいやすい」とかの>>635のいうところの恣意的な理由で
適当な基数をきめて、その組み合わせやら式やらの一定のパターンでもって
数を表現しているわけだよね。（ここは「数学」の本質かな）
１進なら個体の数が直接的にわかりやすいから、
２進ならコンピュータであつかいやすいから、
１０進なら人間にわかりやすいから、
１６進ならコンピュータであつかいやすくて人間にもそこそこわかりやすいから、
という感じ？
こう書くと、この中では１６進が一番恣意的だな。
0639１３２人目の素数さん
2010/03/16(火) 06:48:47ハル これは。。。。。。。。自明だ。QED
0640１３２人目の素数さん
2010/04/08(木) 07:14:590641１３２人目の素数さん
2010/04/08(木) 07:50:13「それならコンピュータに解法プログラムと数式処理プログラムと人工知能を組み込んで問題を解かせることは
可能だと思われますか。もしできるなら、スーパーコンピュータのサーバーサイドに入試問題解説ソフトウェア
を組み込んで富士通のクラウドサービスで配布すれば教育費が安上がりになるはずです。」
http://ameblo.jp/wadahideki/entry-10502592674.html
コンピューターによる定理の自動証明
http://science6.2ch.net/test/read.cgi/math/1126017312/
職業教育訓練用クラウドサービスをお願い。安い通信教育で学べるシステムが必要。
http://jp.fujitsu.com/about/journal/voice/enq/enq1003.shtml
0642１３２人目の素数さん
2010/04/14(水) 18:11:43あとプログラマ向けにhttp://adam.chlipala.net/cpdt/とか
0643１３２人目の素数さん
2010/04/16(金) 17:52:50どうせ本屋に取り寄せて貰っても同じだし、直接springerから買うか…
0644１３２人目の素数さん
2010/04/25(日) 20:37:340645１３２人目の素数さん
2010/04/25(日) 21:11:370646１３２人目の素数さん
2010/05/08(土) 20:35:41＞可能だと思われますか。
計算量理論などの結果からすると難しいと思うが入試問題の解法アルゴリズムについて
考察することは興味深いな。定理証明技法に基づく入試問題攻略本が書けたら売れるだろうな。
0647１３２人目の素数さん
2010/05/08(土) 22:48:380648１３２人目の素数さん
2010/05/08(土) 22:51:50ボーマン。。。アンテナがへんだわ、ちょっとみてきて
0649１３２人目の素数さん
2010/05/29(土) 13:42:260650１３２人目の素数さん
2010/06/11(金) 05:00:370651１３２人目の素数さん
2010/06/11(金) 07:20:56俺にできるチャンスがあるってことだ。
成功したら報告しに来るよ。
0652１３２人目の素数さん
2010/06/25(金) 00:50:58学んで、その結果かなりの定理が自動的に証明できるレベルに達したとする。
だが、如何なる命題を定理に据えて理論体系を構築するのかという部分は、
どうするのか？何が定理として相応しいか、何が単なる証明できる命題という
だけの単なる命題にすぎないのかをどう判定判別するのであろうか？
■ このスレッドは過去ログ倉庫に格納されています