发信人: riverrich()
整理人: (2000-03-30 08:23:54), 站内信件
|
我并不是指代入数值，而是指数学上的逻辑推导了。
事实上，我对这些软件的推导能力表示怀疑。
这些软件的基本思路都是用递归的方式进行搜索。
而每一层都对那么多条的定理和公式代入下一层
的子程序里面，如果不用“剪枝”法必然会有Timeout的
情况出现，某些复杂的证明可能几天也不能证明出来。
但是用了“剪枝”法来处理，可能部分的结果会遗失。
再讲现在的家用计算机的确速度和稳定性存在很大的问题，
这个时候可以讲还没有一只能很高效率地推出一些
复杂的问题的家用软件，反而人对于这些问题的
速度可以比计算机还高。当然处理一些简单的推理，
局限在一些范围里面是没有问题。不过现在的搜索范围
未知道的，而且命题是否正确还不能一眼看出。
假如交给电脑做这方面的东西，据我个人认为风险是
很大的。但如果有超级电脑的话就不同讲法了。
【 在 bsese (b77 行) 的大作中提到: 】
: 【 在 riverrich (居士) 的大作中提到: 】
: : 现在如果用计算机上的数学的推导证明软件，
: : 也很难确保在允许时间内遍历所有解完成必要
: : 的证明过程。用人证明还是必不可少的。
: .......
--
风兮，雨兮，
上网兮，灌水兮。
在风雨兮上网，
与斑竹兮齐灌。
※ 来源:．月光软件站 http://www.moon-soft.com．[FROM: 202.96.190.124]
|
|