09/01/03 09:07:39
>>428
そんなわけねーだろ
432:１３２人目の素数さん
09/01/03 18:49:58
そういえば数学板には数値解析のスレがないね
どっちかといえばシュミレーション板やプログラム板になるのかな
でも理論的なことを語るのに数学板にも一つぐらいあってもいいと思うんだが
433:１３２人目の素数さん
09/01/09 15:19:33
>>432
シュミレーション？？？
大丈夫ですか？
434:１３２人目の素数さん
09/01/09 15:57:52
数学板、誤変換（旧）
○確率
×確立
○置換
×痴漢
○偏微分
×変微分
○整式
×正式
○小数
×少数
○有理化
×有利化
○対数
×大数
（ただし『大学への数学』または"大数の法則"の意の場合も・・・）
○シミュレーション
×シュミレーション
（日本語にない発音のため。ただし方言には近い発音があるらしい）
○キチ（既知）
×ガイチ
（またちなみに、既出（きしゅつ）と読む。"がいしゅつ"ではない。）
435:１３２人目の素数さん
09/01/10 11:21:38
○可算無限
×加算無限
○最大元
×最大限
○単項イデアル整域
×炭鉱胃である聖域
436:１３２人目の素数さん
09/01/11 02:38:33
>>435
一番下ねえよｗｗｗｗｗｗｗ
437:１３２人目の素数さん
09/01/11 23:19:48
>>435 wwww あるある
o 正則行列
x 生息行列
o 単射である
x 単車である
o 閉包を得る
x 兵法を得る
438:１３２人目の素数さん
09/01/12 05:45:54
>>1
無理だろ。
そもそもC言語もVBもmathematicaも、√2の計算すら
どうせどっかで四捨五入してるんだろ？
じゃないと永久に表示できないからな。
定理の証明に四捨五入なんてしたことないぞ、おれは。
439:１３２人目の素数さん
09/01/12 13:57:56
>>438
なんでコンピュータがわざわざ四捨五入とかいう十進法に依存した方法を使わなならんのだ
440:１３２人目の素数さん
09/01/12 14:10:41
２進法なら、零捨一入かな
441:１３２人目の素数さん
09/01/12 16:12:02
>>438
大して知らないのに、知ったかすると恥ずかしいよ。
442:１３２人目の素数さん
09/01/12 19:09:39
>>441
なら答えてもらおうか。
√2の計算は四捨五入するかしないか。
定理の証明において四捨五入するかしないか。
443:１３２人目の素数さん
09/01/12 19:19:37
物理じゃあるまいしなんで証明に無理数の計算が必要なのかと
444:１３２人目の素数さん
09/01/12 20:40:21
PrologのスレにFORTRANが来たって感じだな
445:１３２人目の素数さん
09/01/12 21:09:57
√2の計算がどうとか言ってるやつは高校数学程度までしか知らないの？
446:１３２人目の素数さん
09/01/12 21:17:40
√2は単に x^2-2=0 の根であるということを意味する記号として扱える。
実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
証明に使う性質は、「x^2-2=0 の根である」という代数的性質から全て導かれる。
まあ、実際、代数学の証明の幾つかは既にコンピュータに載せられているものもあるし
人間が既にやった数学的証明は、コンピュータに載せることは可能。
ただし、コンピュータが人間の解いてない数学の定理を証明するような
自動証明ができるかどうかとなると話は別だが。
447:１３２人目の素数さん
09/01/12 23:56:08
>√2は単に x^2-2=0 の根であるということを意味する記号として扱える。
>実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
例えばC言語は10桁目で四捨五入するようになっていると仮定する。
√ｘと√ｙは18桁目までは同じで、19桁目から違う数になるとする。
するとC言語では√ｘ＝＝√ｙとなってしまう。
√○を記号として扱おうがこれは避けることの出来ないものだ。
するとC言語では実数の大小関係が確定できないことになる。
大小関係が確定できないということは、実数における命題のほとんど全ては
証明することができないことになる。
448:１３２人目の素数さん
09/01/13 00:02:17
あ～、こうか。
if(x=!y)
{
while(√ｘ＝＝√ｙ）
{
√ｘの小数点以下を求める処理
√ｙの小数点以下を求める処理
}
}
というわけで>>447は取消ということで。
しかし、コンピューターで証明というのは無理だと思うね。おれは。
449:１３２人目の素数さん
09/01/13 00:08:35
>>447
計算機での証明を行う場合も、四捨五入なんかする必要はない
>>446のように何らかの代数的性質を満たす記号として √ を導入すればいいだけ
√x と √y の大小関係もその代数的性質から証明できる話。
>>448のやり方がそのひとつだな
まあ、コンピュータによる完全な自動証明は無理だが、
人間がやる証明の支援くらいは出来るようになるかもしれないとは思っている
450:１３２人目の素数さん
09/01/13 00:12:51
あ、思ってるというか、このスレで何度も出ているように、
一応コンピュータでの証明支援は既にあることはある。
451:１３２人目の素数さん
09/01/13 11:11:08
数学の知識そのものがお粗末なんじゃないの？>>447は。
452:１３２人目の素数さん
09/01/14 10:26:50
マテカを使った事は無いとみた
453:１３２人目の素数さん
09/01/14 10:58:01
ver3から使ってるよ。
ver4から3次元曲面がマウスでぐりぐりできるようになったよね。
454:１３２人目の素数さん
09/01/14 12:32:49
あれば実数を小数有限桁打ち切りで扱うなんて発想は普通出てこない
455:１３２人目の素数さん
09/01/15 10:05:39
じゃあなにか。
あらゆる実数に関する命題は
具体的数値（1,2,3,4,5,6,7,8,9,0）を全く使用せず
抽象的数値（a,b,cなど）で全て証明することができる。
という定理があるということか？
456:１３２人目の素数さん
09/01/15 10:09:40
少しは数学勉強せーーよ。おめーみてーなやつに長々と説明なんかしたくねーーんだよ。
457:１３２人目の素数さん
09/01/15 10:28:41
とりあえずTrace関数でMathematicaがどういう厳密値計算をやってるか追ってみるといい
458:１３２人目の素数さん
09/01/15 10:30:09
ゲーデル数のようなものを導入すれば可能かもしれないと思ってる。
459:１３２人目の素数さん
09/01/15 10:58:22
>>456
長々と説明なんてしなくていい
そういう定理が「ある」か「ない」か
2文字で済む話じゃないか。
460:１３２人目の素数さん
09/01/15 12:47:08
だって問いが意味不明なんだもの
√2を小数で表した物が具体的数値で√2が抽象的数値だって？
誰の脳内設定だよ 実数の構成も理解して無いだろ
461:１３２人目の素数さん
09/01/15 13:12:28
>>438は√2の計算をどっかで四捨五入せずにできるのかｗ 凄過ぎるｗｗｗｗｗ
462:１３２人目の素数さん
09/01/15 14:36:30
質問自体がトンチンカンなんだよなあ。第一
＞そういう定理が「ある」か「ない」か
に答えてもらえば解決すると思ってんだからなあ。マナカナのどっちが美人かを決めれば
解決すると思い込むのと変わらんよなあ。
結局、バカは自分がバカだと認識することはできないんだなあ。
463:１３２人目の素数さん
09/01/15 15:05:45
>>461
晒しあげ
464:１３２人目の素数さん
09/01/15 15:12:31
>>455は「実数」に「あらゆる」という語をひっつけることの恐ろしさを知らない
465:１３２人目の素数さん
09/01/15 16:51:59
>>462
そんな長い文章はいらない。2文字でいい。
>>464
実数に関する証明はあらゆるをつけなければ意味がない。
たった２，３個の実数で成り立った所で何の意味もない。
∀a∈Rについて成り立たなければそれは実数における定理の資格はない。
抽象的な文字（a,b,c・・・）で解決できるから
具体的な数値など求める必要はないと言ったのはそっちだ。
そういう定理がなければそんな発言は出てくるはずがないからな。
466:１３２人目の素数さん
09/01/15 16:53:40
>>463
どっちが晒しあげられてるかも気付かないのね・・・
467:１３２人目の素数さん
09/01/15 16:59:32
そんなに答えだけが欲しいんなら答えてやるよ
「ない」
というか具体的数値とやらを使用しようがしまいが
あらゆる実数に関する命題を全て証明することはできない
468:１３２人目の素数さん
09/01/15 17:02:32
>>466
晒しあげ
469:１３２人目の素数さん
09/01/15 17:03:53
あげ忘れたｗ
470:１３２人目の素数さん
09/01/15 17:07:27
釣りじゃないんだよね？
Mathematicaで「√3＞√2」を評価したとき
それぞれを小数展開してそれらの各桁を比べてるとでもと思ってるの？
471:１３２人目の素数さん
09/01/15 17:19:29
ならおれの勝ちということで。
ではでは。
472:１３２人目の素数さん
09/01/15 17:22:16
おめ
473:１３２人目の素数さん
09/01/15 17:24:28
>>455の
＞あらゆる実数に関する命題は
は
あらゆる実数に関する「証明済みの」命題は
ってことね。
474:１３２人目の素数さん
09/01/15 17:27:01
ん？ どうした？ 満足したんじゃ無かったのか？
本当に知りたいなら付き合う気はあるけど
言葉遊びがしたいだけなら流石にやる気は無いぞ
475:１３２人目の素数さん
09/01/15 17:43:11
自動翻訳があの程度のレベルなのに数学の定理の自動証明なんて出来るわけない
476:１３２人目の素数さん
09/01/15 17:53:34
自然言語と違って厳密だからね
超数学的なことをせずスピードを問わないのならどうとでもなる
477:１３２人目の素数さん
09/01/15 20:25:35
形式化する段階がかなりウザイだろうな
478:１３２人目の素数さん
09/01/16 01:51:07
おれは言葉遊びなんてしてない。
真実追求しかしていない。
抽象的数値a,bには大小関係が定義されていない。
aとbどっちが大きいか？という問いに意味がない。
アルファベットに大きいも小さいもないからな。
a、bに具体的数値を代入して初めて大小関係が定まる。
ところが、ここの住人は具体的数値を求める必要はないと言う。
じゃあ質問するがaとbはどっちが大きい？
ただしaとbには具体的数値は代入されていないものとする。
ただ、おれは>>448で大小関係はプログラムで求められることに気づき
その部分においてのみ、自らのあやまちは認めたはずだ。
479:１３２人目の素数さん
09/01/16 02:27:10
>>478
晒しあげ
480:１３２人目の素数さん
09/01/16 06:17:04
＞ところが、ここの住人は具体的数値を求める必要はないと言う。
どのレスだよ
481:１３２人目の素数さん
09/01/16 12:16:16
482:１３２人目の素数さん
09/01/16 19:26:59
x,yを、x＜yなる実数とする。
a^2=xを満たす正の実数aと、b^2=yを満たす正の実数bがともに存在するとしよう。
このとき、a≧bと仮定すると、x=a^2≧b^2=yとなり矛盾する。
従ってそのようなa,bが存在すれば、a＜bである。
483:１３２人目の素数さん
09/01/16 22:13:33
バカはほっとこうよ。つまんね。
484:１３２人目の素数さん
09/01/17 02:27:00
＞x,yを、x＜yなる実数とする。
この時点でダメだな。
単なる文字に大小関係は無いの。
ｘ＜ｙとする
なんてやってるということはｘとｙにはなんらかの実数、
つまり具体的数値が代入されていることを予定しているんだろ？
アルファベットに大小関係は無いの。
もうほっとこう。だめだ。
485:１３２人目の素数さん
09/01/17 02:42:12
>>484
（´,_ゝ｀）ﾌﾟｯ
486:１３２人目の素数さん
09/01/17 03:18:41
無限小数表現のことを「具体的数値」とか言ってる中学脳が
吠えてるスレはここですか？
487:１３２人目の素数さん
09/01/17 07:58:27
>>484
晒しあげ
488:１３２人目の素数さん
09/01/17 21:16:41
これってさ、コンピュータに何かを発明させるってのと同じくない？
内燃機関を発明できるか？
どういう構造にしたら効率がよいか、とかは得意だろうけど
仮にできたとして、
内燃機関を発明するアルゴリズムは、内燃機関を知っている何かでなければ構築できないのではないか？
489:１３２人目の素数さん
09/01/17 22:05:18
プログラムというのは
実際に打つ前にフローチャート書く。
（フローチャートを書かなくても、図とか絵とか描いて矢印書いたりして
なんらかのフローチャートもどきは書く）
ならそのフローチャートが証明になっちゃってるじゃん。
490:１３２人目の素数さん
09/01/17 22:33:28
>>489
自動証明ってのは、プログラムを生成するプログラムを書くような
ものなんだよ。
491:１３２人目の素数さん
09/01/17 23:36:28
>>490
そのプログラムはフローチャートでは表すことは出来ないの？
492:１３２人目の素数さん
09/01/17 23:48:14
証明可能な定理に関しては、その証明を見つけ出すアルゴリズムがあるっての
知ってていってんだろうな。
つーか。ゲーデル数化も何もしらなそうだな。
493:１３２人目の素数さん
09/01/17 23:51:30
次の複素数と共役な複素数を言え。「2-8ｉ」
↑教えてください！
494:１３２人目の素数さん
09/01/17 23:53:40
素朴な質問なんだけどそういうのもアルゴリズムって言うの？
アルゴリズムって言うとき、自分の感覚では、証明出来るなら証明し、出来ないなら出来ないと有限ステップでわかるようなものってイメージなんだけど。
495:１３２人目の素数さん
09/01/18 00:09:54
>>493
マルチ
496:１３２人目の素数さん
09/01/18 03:16:45
何の定理でもいいんで
その定理が真であることを求めるプログラムをCでも何でもいいんで
書いてもらえませんか？
ピタゴラスの定理でもいいですよ。
497:１３２人目の素数さん
09/01/18 10:41:50
>>494
いやいや、すまんかった。結局こういうやつ>>496がいるからさあ。ちったあ入門くらい自分でやれ
と言いたくなる。
498:492=497
09/01/18 10:46:57
>>496
少しはヒント出すか。１，２，３，．．．と自然数を順に調べていけば、その中にピタゴラスの定理の証明が
あるんだけど。意味わかんねーだろ。だから、ゲーデル数化ぐらい知っとけっての。
あ、それから、真であることを求めるプログラムじゃなくて、証明を見つけるプログラムな。
真と証明可能の違いくらいも早く知っとけ。
499:１３２人目の素数さん
09/01/18 11:18:47
>>498
うん、わかんね。
真と証明可能の違いはわかる。
真だからといって証明可能かどうかは保障されてないもんな。
でも証明可能なら真ってことだ。
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のような反応をするわけで。
実際に自動証明の研究でやっていることはといえば、特定の分野で
限られた定理の組合せで証明できる範囲に限定して、
前提となる事実・帰結・推論規則としての定理・定理を適用する上でのノウハウ
等を、その範囲に限定して設計された記述言語で記述しておいて、
それらを利用して、人間には比較的簡単に行えるような証明を構築するプロセスを
計算機にトレースさせるというような試み。
つまり、人間にできないような証明を計算機にやらせるなんてことを
いきなり目指してるのではなく、まずは人間の思考というものを
プログラムでモデル化してみることで、人間的な有機的な物事の捉え方を
計算機で応用するための知見が得られないかを探る基礎的な研究であって
本質的には人間工学に近い分野。あとはノレッジベースとかＡＩ（死語）とか。
実際に素材としている数学の分野は、簡単な定理の組合せで証明できる
初等幾何が主流。それも、ピタゴラスの定理のように数値の計算が
からむようなものは「簡単な定理」の範囲に入らない。
503:１３２人目の素数さん
09/01/18 16:46:54
証明可能な命題の集合と有限ステップで証明可能な命題の集合が異なる以上
ゲーテル持ち出しても何の意味もない
504:１３２人目の素数さん
09/01/18 17:20:16
>>503
有限ステップでは証明できないが、証明可能な命題ってあるの？
505:１３２人目の素数さん
09/01/18 20:43:14
ω規則があるならあるでしょうな
506:498
09/01/18 21:48:08
>>502
をを！すまんかった。今は反省している。どうも>>498を読んだときバカにされた気が
して感情的になってしまったようだ。
おわびに、ゲーデル数化をしても、定理の自動証明にはあまり実用的でないということ
を例えで説明しよう。まず、使用する文字を決める。例えば、ひらがな全てでも良い。
カタカナを含めてもよい。いずれにしても使う文字は有限個に決める。例えばN個だと
しよう。文字を2つだけ並べた文字列は有限個しかない。今の例ならN×N個だ。文字を
3つだけ並べた文字列も有限個。4つ並べても有限個。．．．と行くと、いずれは例えば
ふるいけやかわずとびこむみずのおと
というような文字列も現れるし、ピタゴラスの定理の証明として読める文章も現れる。
それに、以上の手続きは簡単なアルゴリズムで書ける。もっと詳しく論理式とか、証明
を定義すれば、任意の文字列に対して、それが何らかの定理の証明になっているかを
判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
あるかどうかの判定をするアルゴリズムも書ける。
507:498
09/01/18 21:49:45
（すまん。上の>>498は>>489のまちがい。）
だからといって、以上の方法が実用的でないということは容易にわかると思う。現在の
コンピューターでは演算速度も記憶容量も足りなすぎる。もちろんいずれ以上のような
方法でも十分実用になるような性能を持ったコンピューターが現れる日が来るかもしれ
ないが、そのころにはの方法で、もっと効率よく定理を証明するアルゴリズムが開発さ
れているかもしれない。
長文すまんかった。失礼。
508:498
09/01/18 21:52:04
あ、実用的でないというのは「たとえ証明可能であることがわかっている命題の証明を探すとしても」
実用的でないということ。
509:１３２人目の素数さん
09/01/19 02:29:07
>ピタゴラスの定理の証明として読める文章も現れる。
なるほど。その発想はなかったわ。
行間を読む行為もしなくて済むだろうし。
要するに定理の証明とは「有限個の文字の羅列」なんだね。
でも、ここで数学をかじってる人間はすぐに一般化したくなると思うんだ。
「無限個の文字の羅列」で表される定理の証明はあるんだろうかとか
「文字と文字の間にじつはさらに文字があるみたいな、実数の稠密性みたいな文字集合」とか。
ところで
数学の定理は有限個の文字で証明できる
という定理はあるの？
510:１３２人目の素数さん
09/01/19 02:32:06
真偽を証明できない命題がある以上そんな定理はないだろ
511:１３２人目の素数さん
09/01/19 02:33:51
数学基礎論でいう定理の自動証明ってのは>>498が言うようなものじゃないんだが
512:１３２人目の素数さん
09/01/19 03:03:50
スレタイと１の延長で話してるなら、基礎論が出てくること自体おかしいってことだろ
513:１３２人目の素数さん
09/01/19 11:10:46
有限個の文字の羅列でも
文字数が確定していないんだから
文章の数は無限個だから証明の文章はできないんじゃないの？
ある定理は100文字で証明終わりになるとはじめからわかっているなら
100個の文字のあらゆる組み合わせを調べつくせば済むけど
その定理の証明が100文字で終わることをどうやって事前に知るの？
514:１３２人目の素数さん
09/01/19 11:11:49
基礎論の一分野として自動証明をしてる人もいるから
>>498が話してるような方面の基礎論は関係なしで
515:１３２人目の素数さん
09/01/19 11:26:46
あ.あ
あ.いうえおか
か.なにぬね
こういう文字集合を定義したら
証明できる命題は増えるんでしょうか？
516:１３２人目の素数さん
09/01/19 12:09:49
>>505
ω規則ってどんなのですか？
517:１３２人目の素数さん
09/01/19 12:57:53
わかってないなぁ。
科学が信仰する事実そのものという観念は、宗教、特にキリスト教の神観念に近い。
これは科学が西洋社会を起源にもつ文化現象であるという一つの証拠である。
キリスト教の神観念は、人間の外にある絶対者であり、人間にとって認識不可能かつ到達不可能な存在である。
これは正しく科学が前提とする事実そのものの存在と同じである。
ちみなに、仏教では一切の存在に仏の生命が宿ると考える。
仏性=真理は外にある絶対のものではなく、個々の存在に宿る内面的なものである。
真理は自身のうちにあり、外にはないと考える。
科学は真理を人間の意識の外に求めようとする点において、極めてキリスト教的、西洋的である。
到達不可能な絶対者を立てる科学は、キリスト教と同型の思考形態をもつ。
真理そのものがはなから自己のうちに宿ると考える仏教的発想によって、科学は相対化されるのである。
また、構造構成主義もシステム論も、意識から隔絶した事実そのものを定立することなく、世界を記述するので、科学とは観察方法が根本的に異なることになる。
518:１３２人目の素数さん
09/01/19 17:34:35
誤爆か？
519:１３２人目の素数さん
09/01/19 18:18:18
いいえ、スパです
520:１３２人目の素数さん
09/01/20 02:29:24
おいおい、逃げるなよ。
文字に大小関係を導入したとたんに逃げるか。
おれだよ、おれ。
文字に連続性を持たせたとたんに口を閉ざすか。
もっとさらし上げろよ。
521:１３２人目の素数さん
09/01/20 10:45:36
お前一人で何の話してるんだ
522:１３２人目の素数さん
09/01/22 03:03:35
>使う文字は有限個に決める
だから使う文字を有限個にしたところで
出来上がる文章は無限個だろ。
そんなロジックもわからないのか。
あ
ああああ
ああああああああ
ああああああああああああああ
わかるよな？
あだけで無限個文章があるよな？
まさか逃げはしないよな？
523:１３２人目の素数さん
09/01/22 04:04:15
だからどうした
524:１３２人目の素数さん
09/01/22 20:00:18
そんなに十進表記が大好きでそれで上手くいくと思ってんならそれでやってけばいいよ
グッドスタインの定理を途中に出てくる式全部きっちり計算して証明すればいいし
チャイティンの定数も十進表記で計算し終わってから議論すればいい
525:１３２人目の素数さん
09/01/23 02:11:29
おいおい、本当に逃げちまったよｗｗｗ
526:１３２人目の素数さん
09/01/23 05:55:36
アホ過ぎワロタ
527:１３２人目の素数さん
09/01/23 14:16:25
>>525
晒しあげ
528:１３２人目の素数さん
09/01/24 01:52:30
>>527
よく戻ってきたな。
じゃあ話を聞かせてくれ。
ゆっくりでいいぞ。
緊張しなくていいんだぞ。
529:１３２人目の素数さん
09/01/24 05:05:11
>>528
晒しあげ
530:１３２人目の素数さん
09/01/24 09:49:08
＿,====ミミﾐヽ、
,,==≡ミヽミヾミミミ、ヾ、
_=≡≡三ミミﾐ ミﾐヾ、ソ)),,》 .
彡彡二二三≡ミ-_ ﾐﾐ|ノﾉj )||ヽ, )、
__,,,,,,,,,／彡二二二 ,- __ﾐ|/ﾉ ﾉﾉﾉﾉ) ||
-=二ミミミミ----==--'彡 ∠ミﾐ_ソノノノﾉ ﾉ
/／＞=''"二二=-'"_／ ノ''''')λ彡／
,,/￣''l 彡/-'''""￣-=彡彡／ ,,-''",,,,,,,ノ .彡''"
(, ,--( 彡 ,,-- ===彡彡彡"_,-＿ ヽ Υ
ヾ-( r'''''＼ ／／=二二''''''彡ｿ￣ ∠__＼ .＼ｿ .|
＼;;;; ＼ Ζ彡≡彡-'''',r-､> l_"t。ﾐ＼ﾉ,,r-v ／￣￣￣￣￣￣
＼;;;; ＼ 彡""彡彡-//ヽ" ''''''""￣'''""(ｴｱ/ ／
＼;; ＼'''''')彡ヽ// | (tv ／| , r_>'| ＜一体みんな誰と戦っているんだ
＼;;; ＼'" ＼ ,,"''-,,ﾉ,r-", / r'''-, .j ＼
＼;;; ＼ ／,,>--'''二"''' r-| 二'" / __ ＼＿＿＿＿＿＿
＼;;r'""彡_l:::::::::::::::::::::: /./_ " ／￣￣"===-,
)''／／rl_--::::::::::::::::/:/ヽ"'=--":
531:１３２人目の素数さん
09/01/26 09:39:21
>任意の文字列に対して、それが何らかの定理の証明になっているかを
>判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
>あるかどうかの判定をするアルゴリズムも書ける。
ええ、うそでしょ？
ならそのアルゴリズムがすでに定理の証明になっちゃってるじゃん。
532:１３２人目の素数さん
09/01/26 12:00:37
>>531 この>>506が言っている3行は事実。証明と定理がラムダ計算の式と型に対応しているという理論(Curry-Howard対応)
を使えば、ある文字列(式)がどのような定理(型)を証明しているか、それとも間違っている(型エラー)か自動判定することができる。
しかし、逆に、定理(型)からその証明(式)を導くことは完全自動では無理。
533:１３２人目の素数さん
09/01/26 14:35:49
高校レベルの問題なら、自動的に解いてくれるプログラムが完成したよ！もちろん、定理の証明も可。
問題を入力すると、その問題を２ちゃんやYahoo!やOKWaveとかの質問スレに自動的に書き込んで、結果を読み込んで戻ってくる。
そういう掲示板だけでなく、あらかじめ指定したアドレスへ質問メールを出して、返答を受けることも可能。
これで殆ど解決。
でも最近、回答の精度が落ちてるんだよなあ。「マルチポストはヤメレ」「質問ばかりするな」なんていう意味のない回答が良く来るようになった。
どうしてこうなったんだろう。プログラムのミスかなあ。
この辺をどう解決するかが今後の課題。
534:１３２人目の素数さん
09/01/26 17:47:35
>>532
虱潰せばできるけどね
簡単な定理でも地球が滅びるくらいの時間が掛かるだろうけど
535:１３２人目の素数さん
09/01/26 19:46:43
talk:>>533
それは反則ではないのか？
536:KingGold ◆3waIkAJWrg
09/01/27 18:05:14
Reply:>>533 その計画書を私に見せてみろ。
537:１３２人目の素数さん
09/01/27 23:14:04
トースターによる定理の自動コピーとか
証明はDNAパソコンでしょ
538:１３２人目の素数さん
09/01/27 23:16:47
>>533
そういうソフトはすでに存在しているんじゃね？
オープンにされてないだけで。
簡単につくれるし。
539:１３２人目の素数さん
09/01/27 23:26:43
「九九」の歴史は古く、中国の春秋時代（紀元前七七〇年から紀元前四〇三年）にまで遡ります。春秋五覇の一番目、斉の桓公（B.C.685-643) が人材を求めた時に、「九九」 を暗記しているという特技で採用された者がいたという記事が残っています。
540:１３２人目の素数さん
09/02/06 10:13:49
大学入試レヴェルの『数学的帰納法』を
プログラムによって解かせるものを考えた。
でもこれって既出かな？？？
541:１３２人目の素数さん
09/02/07 08:19:23
マジで!
ソースきぼんぬ
542:１３２人目の素数さん
09/02/07 10:07:42
どうせ再起呼出し使うだけなんじゃねーの
543:１３２人目の素数さん
09/02/07 10:14:34
コンピューターの完全寿司ロボットをつくれば世界に売れる。
ネタの仕込みからにぎりまで
そばロボットもいい
544:540
09/02/07 10:29:02
確かに、簡単なものしか使っていないから既出だと思った。
『数学的帰納法』で
１．等式の証明
２．不等式の証明
があるけど
正の整数（自然数）のみ動かせば
負の整数の場合も自動的に掃きだしてくれる。
545:１３２人目の素数さん
09/02/11 08:53:40
>>540 \forall n \in N, P(n).
の証明を
P(0) かつ \forall k \in N, (P(k) => P(k+1))
を使って自動証明するってことだよね。
具体的にどんなことが自動でできるの？kwsk
546:１３２人目の素数さん
09/02/11 17:31:47
あたりまえだがすべてのnについて計算するわけじゃない
論理的に式変形をしてしらみつぶしに解いていくだけ
547:１３２人目の素数さん
09/02/11 23:16:09
>>546 x + y = y + x
とかも自動証明できたりする？
548:１３２人目の素数さん
09/02/12 11:49:28
>>547
ぜひどうなるか知りたいね。
549:１３２人目の素数さん
09/02/13 00:10:01
>>547
∀x, ∀y, x + y = y + x が自動で証明できたら
かなりすごいんじゃね？
550:１３２人目の素数さん
09/02/13 00:23:06
>>549
そんな単純な問題なら一瞬で証明できるわな
551:１３２人目の素数さん
09/02/13 00:25:29
>>550
してくれ
552:１３２人目の素数さん
09/02/13 00:46:34
>>550 してくれ
553:１３２人目の素数さん
09/02/13 11:00:44
>>550
してくれ
554:１３２人目の素数さん
09/02/13 16:27:06
>>550
して。
555:１３２人目の素数さん
09/02/13 16:42:42
>>550
頼む
556:１３２人目の素数さん
09/02/13 18:17:40
しらみつぶしってことはどうせ簡単な定理を証明するにも宇宙の寿命ぐらいの時間が掛かるんだろ？
557:１３２人目の素数さん
09/02/13 18:54:35
dim x as string
dim y as string
dim + as string
でできるじゃん
あとは配列にいれてソートしてイコールになればＱＥＤ
558:１３２人目の素数さん
09/02/14 00:17:14
定理の自動証明はＣＵＴ規則で空節が導出されりゃよい。
559:１３２人目の素数さん
09/02/14 00:36:23
>>557
わからん kwsk
560:１３２人目の素数さん
09/02/14 00:52:19
確かＰ算術とかいう簡単な演算体系の定理を証明するのに非決定性アルゴリズムで2重指数時間かかるという定理があったな。
定理の証明を実際的な時間で証明するのは何らかの支援が必要でしょうな。
561:１３２人目の素数さん
09/02/14 03:20:08
コンピュータに出来る訳がないだろwwww
562:１３２人目の素数さん
09/02/14 03:35:03
>>560
2重指数時間かぁ・・・
それは絶望的だな
563:１３２人目の素数さん
09/02/14 09:19:12
2重指数時間でも自動で出きるのはすごいと思う。
>>549なんかはxとyの組み合わせが無限にあるから、有限時間には終わらない。
564:１３２人目の素数さん
09/02/14 13:45:43
2つの関数が等しいか否かのチェックって決定不能問題だよな
565:１３２人目の素数さん
09/02/14 16:42:35
将棋や自然言語処理のように、いっぺんコーパスの料理の仕方が分かれば劇的に進歩するだろうな。
566:１３２人目の素数さん
09/02/14 18:49:33
>>549なんて幅優先探索でλ計算すればすぐに解けるじゃん
567:１３２人目の素数さん
09/02/14 22:46:50
プログラムは可算個しかないのに、決定問題は非可算個存在する。
決定不能問題のほうがはるかに多い。
568:１３２人目の素数さん
09/02/14 23:19:48
でも記述可能な決定問題は可算個しかないからねｗ
569:１３２人目の素数さん
09/02/14 23:51:18
計算尺があるだろ！
570:１３２人目の素数さん
09/02/15 00:28:55
誰にレスしてるんだ？
571:１３２人目の素数さん
09/02/15 22:02:38
KLEENEの階層を数学者ががんばったのは計算不可能な領域が広大だと思ったからだろう。
572:１３２人目の素数さん
09/02/15 22:23:29
計算尺で計算量を測るという発想はおもろいね。
573:１３２人目の素数さん
09/02/15 23:49:35
「帰納的集合」だけに限っても計算量的にはかなりでかいクラス
EXPTIMEとかも余裕で含むので「現実的には計算不可能な」
証明がほとんどと見なして差し支えないかと。
574:１３２人目の素数さん
09/02/16 03:15:48
しかし計算量では多項式時間かどうかが重要なようだが２乗もあれば追い付けなくないか？
575:１３２人目の素数さん
09/02/16 18:34:58
計算時間に関してはO(n^2)のアルゴリズムは十分実行可能であることが多い。
世の中から単純ソートが無くならない所以。
数値解析や数理計画のように実行回数が少ないものはO(n^3)でも歓迎されるくらいだ。
空間計算量の方はもっと厳しくて、理論上指数時間のアルゴリズムでも、
実用上はメモリの制約の方が先にやってくるというのはよくある話。
576:１３２人目の素数さん
09/02/16 19:03:20
定理の自動証明だと定理パターンの組み合わせの適用で解くから
しらみつぶしにやると当然指数的に増加していくな
577:１３２人目の素数さん
09/02/16 22:51:30
ソフト開発の現場にいる連中はアルゴリズムの計算量を議論することってあるのかな。
578:１３２人目の素数さん
09/02/16 23:35:56
>>575
うーん、やっぱり２とか３まで現実的か・・・
例えばＲＳＡが多項式時間で解けるようになったとして、何乗ぐらいから無意味になるの？
579:１３２人目の素数さん
09/02/19 02:35:00
定理の証明をしらみつぶしって解析学では不可能だろ。
実数だから、0、0.1、0.001とかしらみつぶしにしても永久に１までたどり着けない。
離散数学なら4色問題とかでできるんじゃないかな。
580:１３２人目の素数さん
09/02/19 04:06:53
>>577
？？？
処理のエンジン部分を開発しているチームは、日々それと格闘しているだろ。
ループの回し方１つで、処理時間のオーダーが変わる世界。
>>579
変数に代入する値をしらみつぶしとはだれも言ってないと思うが。
581:１３２人目の素数さん
09/02/20 03:27:49
そもそもメモリーセルがON,OFFの離散だから
連続を扱えるはずがない。
お絵かきソフトで直線を書いてもドットの粒が並んでるだけだよ。
直線は絶対にかけないよ。
それどころか紙と鉛筆ですら直線は書けない。
鉛筆の分子が有限個、紙の上に並んでいるだけだから。
というかこの世は離散だから解析学は滅びるべきだよ。
実数も。
582:KingGold ◆3waIkAJWrg
09/02/20 03:30:16
Reply:>>581 それでは現象を表現する方法を述べよ。
583:１３２人目の素数さん
09/02/20 03:34:15
>>582
お前がやれカス
584:KingGold ◆3waIkAJWrg
09/02/20 03:40:20
Reply:>>583 実数を使う。
585:１３２人目の素数さん
09/02/20 07:35:08
>>頭の良い皆さん
ムカつく奴が計算自慢してます。どうか、皆さんでそいつをギャフン(死語ｗ)と言わせてくださ！
板は・スロットサロン
スレは・しのけん
ですm(__)m
ちなみに…∫[-∞,∞]cosbxdx/(x^2+a^2)の値を求めよ、は？
みたいなのを出して答えられないとバカにしまくり。どうか、よろしくお願い致します！m(__)m
586:KingGold ◆3waIkAJWrg
09/02/20 14:15:08
Reply:>>585 そもそもお前はスロットサロン板で何をしている。
587:１３２人目の素数さん
09/02/20 23:19:23
22
588:１３２人目の素数さん
09/02/21 00:34:01
kingってものすごく頭悪いんですね。知りませんでした。がっかりです。
589:KingGold ◆3waIkAJWrg
09/02/21 17:02:48
Reply:>>588 複素解析くらい知りている。お前に何がわかるというか。
590:１３２人目の素数さん
09/02/22 00:44:02
ではkingよ複素解析について語ってくれ
591:KingGold ◆3waIkAJWrg
09/02/22 00:47:52
Reply:>>590 Cauchyの積分定理、Cauchyの積分公式。
592:１３２人目の素数さん
09/02/23 10:26:02
>>585
マルチ
593:１３２人目の素数さん
09/02/28 19:31:02
>>この世は離散だから解析学は滅びるべきだよ。
ものの長さや、時間の流れは連続だが。
偏った"この世"じゃねーか？
実数の公理を使えば、コンピュータでも実数の性質を扱うことは出きるだろ。JK。
594:１３２人目の素数さん
09/02/28 19:50:14
>>593
長さにも時間にもプランク単位、即ち最小単位があるだろ
どんな長さや時間もプランク単位の自然数倍、連続じゃないよ
595:１３２人目の素数さん
09/03/01 09:40:59
URLﾘﾝｸ(ja.wikipedia.org)プランク定数
｜最近では Zurek その他の研究で、量子カオス系においてはプランク定数以下のミクロ構造が現れる事が知られており、まだプランク定数の正体はよく判っていないと言えるだろう。
596:１３２人目の素数さん
09/03/01 09:52:47
>>594
１プランク長 = 1.616252... × 10^(-35) [メートル]
って時点で、1メートルがプランク単位の自然数倍じゃないよ。
1メートルってのは実は存在しない長さなの？
597:１３２人目の素数さん
09/03/01 18:25:45
ちなみにプランク質量は 0.02ミリグラム と意外にでかい
598:１３２人目の素数さん
09/03/01 19:08:04
プランク単位を勘違いしてた>>594ﾌﾟｷﾞｬｰということで
599:１３２人目の素数さん
09/03/03 00:32:30
>>597
ミジンコの体重がおおよそそれくらい。だからプランクトンと…
600:１３２人目の素数さん
09/03/06 13:51:43
６００
601:１３２人目の素数さん
09/03/06 13:52:39
６０１
602:１３２人目の素数さん
09/03/07 13:11:32
>>599
座布団一枚
603:１３２人目の素数さん
09/03/09 16:10:20
>>549
うん、それ無理。
ペアノの公理系で、加法の交換法則は定義されてるの。
この公理をペアノの公理系の内部で定理として証明するのは
不可能だったはずよ。
604:１３２人目の素数さん
09/03/09 22:01:17
イミフ。っつーかバカ？
605:１３２人目の素数さん
09/03/10 01:18:03
>>603
> >>549
> うん、それ無理。
>
> ペアノの公理系で、加法の交換法則は定義されてるの。
> この公理をペアノの公理系の内部で定理として証明するのは
> 不可能だったはずよ。
ゴルァ、シレっとウソつくんじゃねえｗｗｗｗｗ
『ペアノ数の概念について』（小野勝次・梅沢敏郎 訳・解説）、共立出版
のp.111に９という番号の付けられた
a, bεN . ⊃ . a+b=b+a
って式が定理として挙げられてるぞ。ペアノ自身の証明はそれを見ろ。
606:１３２人目の素数さん
09/04/05 16:11:55
機械に証明が出来ないなら
脳は分子機械に過ぎないのだから
証明は心霊現象になってしまう
607:１３２人目の素数さん
09/04/08 20:10:51
自動定理証明
URLﾘﾝｸ(ja.wikipedia.org)
にでてる「ハーブランド賞」てエルブランじゃね？
608:１３２人目の素数さん
09/04/09 05:28:18
>>607
Herbrandの仏語の音をカタカナで近似すれば「エルブラン」、
英語読みした音をカタカナ書きすれば「ハーブランド」
609:１３２人目の素数さん
09/04/26 22:10:30
polytypic programming in coqに載っている以下の例
Coqのバージョン8.2ではコンパイル出来ないんですが
なぜだかわかる方居ますか？
このPDFはかなり面白そうな感じがするんですが
実際に動かせないので悲しいです
別のバージョンだと動いたりするんでしょうか
Fixpoint tupleT (A:Type) (n:nat) : Type :=
match n with
| O => unit
| S m => A * tupleT A m
end.
全般的に依存型に関する情報が少ないもので困ってます
610:１３２人目の素数さん
09/05/03 08:30:48
>609
Open Scope type_scope.
の１行を最初に書くと私の環境ではコンパイルとおりました。
Coq 8.1pl2 と8.2 でコンパイルが通ったことを確認しました。
611:１３２人目の素数さん
09/05/03 11:27:41
>>581
ベジータ「数学は科学基礎だ!!
舐めるなよー!!!!｣
>>595
宇宙→銀河系→太陽系→惑星→分子→原子→素粒子→クォーク→…
無限階層説があるのう｡
612:１３２人目の素数さん
09/05/05 00:30:01
>>610
動きました!
諦めかけてたのですが、ありがとうございます!
613:１３２人目の素数さん
09/07/08 17:10:04
URLﾘﾝｸ(twitter.com)
614:↑
09/08/11 21:15:59
ブラクラ危険
615:１３２人目の素数さん
09/08/15 13:26:46
「gallina coq 勉強」でググったらこんなの見付けた！
定理証明支援系と依存型プログラミング勉強会
URLﾘﾝｸ(tzik.homeunix.net)
616:１３２人目の素数さん
09/08/15 17:37:17
>>1
> コンピューターによる定理の自動証明
> これが可能になったら数学者という仕事が無くなっちゃうの？
1 にマジレスすると、自動証明できる空間は非常に小さくて、ほとんど意味が無い。ということが証明されている。
むしろ多くのひとが興味のあるような命題は機械の支援に加え人間の手が必ず必要になる。
これは普通の数学だとあんまりうれしくない事実だけど、コンピュータの動作の保証が得られることは、プログラムの世界では
非常に重宝される技術。例えば、原子力施設のプログラムや、鉄道や道路の信号のシステム、医療、金融関係のシステムは不具合が許されない。
結論を言うと、定理証明の技術が発展すれば、数学者はプログラムの基幹システムにおいて、むしろ必要不可欠になる。
だから、数学者はプログラム技術を、プログラマは数学をしっかり学んでおくと将来お徳だと思う。
以上が私の妄想。
617:１３２人目の素数さん
09/08/21 22:58:47
だれか超現実数全体が有理数全体より大きいことの証明を教えてください。
618:１３２人目の素数さん
09/08/22 11:03:50
実数は超現実数の範囲で表せる
実数の集合は有理数の集合より大きい濃度を持つ
619:１３２人目の素数さん
09/09/07 00:35:12
四年一時間。
620:１３２人目の素数さん
09/10/13 21:35:41
coqの質問はここでいいでしょうか？
よくある論理パズル（正直者と嘘つきがいて、ある人が～と言った。とかいうやつ）を
coqで解きたいと思ったのですが
要するに命題論理の式をCNF(乗法標準形？）に変形できればいいのですが
coqでうまくやる方法をご存知の方いますか？
621:sage
09/10/15 16:29:24
>>620 命題論理のCNFへの変換のような問題であれば、証明器でなくてもプログラムで実装できると思います。
622:sage
09/10/15 16:31:57
>>620 その変換の実装の正しさを検証するのであればCoqは非常に適していると思います。
623:１３２人目の素数さん
09/10/16 00:37:23
はい、そういう検証もたいへん興味をそそられるのですが、
元の質問の動機は、スマリヤンの本の序盤のパズルを
覚えたてのcoqを電卓がわりに使って解けないかというぐらいのものなので、
ちょっと問題が大きい感じです。
hnfというtacticが標準であるので、
他の標準形にもちょいちょいと直せないものかと思った次第です。
624:sage
09/10/16 08:03:11
>>623 スマリヤンの本をよく知らないのですが、どのようなパズル問題ですか？
625:１３２人目の素数さん
09/10/16 12:19:06
>>624
Wikipediaにまとめがありました。
URLﾘﾝｸ(en.wikipedia.org)
日本語なら
URLﾘﾝｸ(www.kai.ed.jp)
というのが検索で出てきました。
よくあるパズルとか書きましたが、
スマリヤンがオリジナルなのかもしれません。
626:１３２人目の素数さん
09/11/02 13:37:58
てｓｔ
627:１３２人目の素数さん
09/11/03 05:57:33
どうも、「ＥＵＲＭＳ（∋ M_SHIRAISHI氏 ）の理論」のほうが正しいようだな。
例えば、《仮言三段論法の原理》は、従来は、 [(Ｐ⊃Ｑ)＆(Ｑ⊃Ｒ)]⊃(Ｐ⊃Ｒ) で
表わされるもののことと考えられていたのだっただが、これは、どうやら、誤りだった
ようだ。
そして、ＥＵＲＭＳの言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)]＆[Ｑ(ｘ)⇒/x/Ｒ(ｘ)］⇒/p,q,r/［Ｐ(ｘ)⇒/x/Ｒ(ｘ)] 1{Ｑ」
こそが、《仮言三段論法の原理》を 正しく捉(とら)えてたものと考えられる。
ＥＵＲＭＳの主張する「論理＊大＊改革」は、恐らく、世界を席巻することとなろう。
URLﾘﾝｸ(www.age.ne.jp)
628:１３２人目の素数さん
10/02/04 17:16:30
806
629:１３２人目の素数さん
10/03/02 21:35:27
>>596
1年前のレスだが、1mがプランク長の整数倍じゃないのは誤差だから。
630:１３２人目の素数さん
10/03/02 22:19:16
電荷1Cも電気素量の整数倍じゃない。1.5倍とかなら素量として使えないが指数表現レベルなら
厳密な整数倍じゃないのは単なる誤差
631:１３２人目の素数さん
10/03/02 22:43:53
そのうちクーロンの定義が素電荷の整数倍になるかも
632:１３２人目の素数さん
10/03/06 01:03:58
プランク長が最小の長さならルベーグ測度は無意味じゃない？
633:１３２人目の素数さん
10/03/06 02:30:58
>>632
それを言うならば、そもそも選択公理を用いた数学で物理理論を記述してるのがナンセンスなのだが
フルスペックの選択公理はBanach-Tarskiのパラドックスを導いてしまうからね
>>631
うん、例えばクーロンの定義が電気素量ｅの１Ｎ（アボガドロ数）倍（つまり１モルの陽子の電荷総量）なら明解なんだけどね
現在は電流単位としての１Ａ（アンペア）をその電流が流れる電線の間の力の強さで定義して
１Ａの強さの電流で１秒流れる電気量を１Ｃ（クーロン）として定義してるからなあ
質量の単位のｋｇについても今のキログラム原器なんて怪しげというか恐ろしく原始的な定義じゃなくて
炭素１２原子核の質量の１Ｎ倍を１２グラムとして定義しようというアイデアはかなり昔からあるんだよな
あるいは陽子（普通の軽い水素の原子核）の質量の１Ｎ倍を１ｇと定義すればもっと明解だな
炭素１２原子核にしろ陽子にしろ、そういうものの質量なら質量分析器を用いて極めて精密に測れるからね
今は逆にアボガドロ数の定義として１２ｇの炭素１２に含まれる炭素１２の原子数を用いていたんじゃないかな
（つまり上の新しい定義の提案だと、アボガドロ数は実験で決まる定数でなく最初から値を定めておく定数にせねばならない）
634:１３２人目の素数さん
10/03/06 23:28:10
科学的で合理的な単位系はプランク単位系。もっというなら数値も16進数が合理的。（プランク単位系でなおかつ16進数）
10進数は人間の指の数が起源だからある意味原始的。日常生活での16進数への移行は難しいが
635:１３２人目の素数さん
10/03/09 13:08:15
プランク単位系には物理的な裏付けがあるが、
数はどの底をとっても恣意的でしょう。
もっというなら16進数よりは2進数のほうが本質だと思う。
636:１３２人目の素数さん
10/03/10 22:09:12
e進法ができないのは不便だな。角度だってラジアンのほうが数学的に便利だから数学では度数法に取って変わったわけだし
637:１３２人目の素数さん
10/03/15 12:27:50
一進数、つまり数の個数分だけ１でも何でも良いから記号を書き並べる
のが本質。但しこれだと０を表すことができないので、
個数に１個げたを履かせることで回避するようなことをしなければ
ならない。
たとえば
０： ×
１： ××
２： ×××
１０： ×××××××××××
。。。。
638:１３２人目の素数さん
10/03/16 01:21:49
それだと何かの数の整数倍しか表現できなさそうだけど、どうかな。
底とかナシで無限個のシンボルをつかって表現するのが本質なんじゃない？
つまりどの数も違うひとつの記号で表されるって感じで。
実際は、これを実現するのが無意味に大変だから、
「わかりやすい」とか「つかいやすい」とかの>>635のいうところの恣意的な理由で
適当な基数をきめて、その組み合わせやら式やらの一定のパターンでもって
数を表現しているわけだよね。（ここは「数学」の本質かな）
１進なら個体の数が直接的にわかりやすいから、
２進ならコンピュータであつかいやすいから、
１０進なら人間にわかりやすいから、
１６進ならコンピュータであつかいやすくて人間にもそこそこわかりやすいから、
という感じ？
こう書くと、この中では１６進が一番恣意的だな。
639:１３２人目の素数さん
10/03/16 06:48:47
ハル これを証明してくれ。
ハル これは。。。。。。。。自明だ。QED
640:１３２人目の素数さん
10/04/08 07:14:59
mizarやcoqの入門書とかないもんかね
641:１３２人目の素数さん
10/04/08 07:50:13
スーパーコンピュータで入試問題を解答できるか
「それならコンピュータに解法プログラムと数式処理プログラムと人工知能を組み込んで問題を解かせることは
可能だと思われますか。もしできるなら、スーパーコンピュータのサーバーサイドに入試問題解説ソフトウェア
を組み込んで富士通のクラウドサービスで配布すれば教育費が安上がりになるはずです。」
URLﾘﾝｸ(ameblo.jp)
コンピューターによる定理の自動証明
ｽﾚﾘﾝｸ(math板)
職業教育訓練用クラウドサービスをお願い。安い通信教育で学べるシステムが必要。
URLﾘﾝｸ(jp.fujitsu.com)
642:１３２人目の素数さん
10/04/14 18:11:43
coqの入門書はCoqArtがあるじゃない
あとプログラマ向けにURLﾘﾝｸ(adam.chlipala.net)とか
643:１３２人目の素数さん
10/04/16 17:52:50
Coq'Art売ってねぇじゃねぇか
どうせ本屋に取り寄せて貰っても同じだし、直接springerから買うか…
644:１３２人目の素数さん
10/04/25 20:37:34
プランク定数ってフォトンでやったときだろ。クオークだったら話が変わるぞ。
645:１３２人目の素数さん
10/04/25 21:11:37
たいとるが コンピューター君による自演スレ にみえたW