コンピューターによる定理の自動証明
■ このスレッドは過去ログ倉庫に格納されています
0447132人目の素数さん
2009/01/12(月) 23:56:08>実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
例えばC言語は10桁目で四捨五入するようになっていると仮定する。
√xと√yは18桁目までは同じで、19桁目から違う数になるとする。
するとC言語では√x==√yとなってしまう。
√○を記号として扱おうがこれは避けることの出来ないものだ。
するとC言語では実数の大小関係が確定できないことになる。
大小関係が確定できないということは、実数における命題のほとんど全ては
証明することができないことになる。
■ このスレッドは過去ログ倉庫に格納されています