关于几何解题软件。
近来媒体报道几何解题软件与教师比赛的事，软件在速度上占有优势，教师在技巧上占有优势。好象软件具有逻辑思维能力一样，有没有高手能给讲讲具体的算法原理。思路也行。 问题点数：50、回复次数：8Top
1 楼wanbaocheng（www）回复于 2002-05-30 17:05:12 得分 10
不知听说过吴文俊这个人没有。他是我国著名的数学家。他开创了数学机械化的先河，通过他发明的算法可以用计算机来解决初等几何题。你所说的几何解题软件应该用的就是这类算法。Top
2 楼nethermit（网络隐士）回复于 2002-05-31 10:44:05 得分 0
这几天报纸上猛吹啊，几个顶尖几何牛人要1小时，这软件要6秒钟。
我表示持怀疑态度，因为中国的这帮媒体记者素质太差，根本不懂这行的事情，胡吹猛侃是可能的。Top
3 楼wanbaocheng（www）回复于 2002-05-31 11:55:47 得分 0
我虽然没有看到这个报道,但我相信是真的.原因如我上面所说.Top
4 楼Xcoder（流浪狗）回复于 2002-06-03 11:36:39 得分 10
这篇文章我也看了，我想，首先应该有一个数据结构，用于表示几何定理。包括条件和结论。然后采用逆向回溯的办法，遍历每一个结论为索要证明的命题的结论的定理，再看这些定理的条件是否为已知的命题条件，否则在同样查找可证明该条件的定理，直到所有条件为已知条件。
不过这似乎只堆几何证明题有用，要计算就更繁了。Top
5 楼wanbaocheng（www）回复于 2002-06-03 17:48:10 得分 0
你有想法挺好，但是按你这样是行不通的。过程是先把几何问题转化为解析几何的问题，也就是几何问题代数化，然后用数值方法（这个方法后面有定理的支持，不是随便的，总之是把一个无限次验证的问题有限化，具体不说了）来证明命题的正确性。大体思想就是这样。Top
6 楼starfish（海星）回复于 2002-06-03 22:21:10 得分 30
对定理证明自动化的研究现在已经比较成熟了
早在60年代就已经证明了所有的初等几何定理都可以由计算机自动证明。
其基本思想是利用形式化的公理系统，将基本公理看作节点，规则看作由某些节点生成另外一些节点的条件，定理证明的问题就转化为在隐式图中从初始节点（基本公理）出发，根据生成规则找到到达目标节点（要证明的定理）的一条路径。可以利用各种隐式图搜索算法来解决这个问题。Top
7 楼Xcoder（流浪狗）回复于 2002-06-04 15:13:01 得分 0
用解析几何的方法，人能看懂吗？该软件是面向大众的，如只给出数值计算的结果，对几何教学有何益处？大家还是来讨论一下用什么数据结构表示定理吧。Top
8 楼goodsong（风卷残云~不要把简单的事搞得N复杂）回复于 2002-06-04 23:09:20 得分 0
upTop
