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