应该是属于 数理逻辑 吧
ML程序设计语言是较少的讲这个的程序设计的书 今天在图书馆看了两本几何定理机器证明的书，以前的模糊得到了澄清。
说到几何定理机器证明，其实应该提到三个人，吴文俊，张景中，杨璐。
吴文俊的证明，核心是"吴法"，但最终返回的结果是命题的真与假，至于中间过程具体是怎样的，被软件处理成了黑箱子，我们无从知晓。
而张景中的是改进版的，核心是消点算法，是可读证明。
前面二人的方法只能证明等式的命题，而杨璐的降维算法可以证明不等式，其应用领域也由几何扩充到代数了。 原帖由 wayne 于 2009-3-20 12:03 发表 http://bbs.emath.ac.cn/images/common/back.gif
你是说 涉及到了自然语言的谓词处理吧，可我好像记得我们中国的吴文俊之 “吴氏消元法”可以办到，.....
自然语言处理这部分，我当时没搞清楚，说的有点问题。
下面是MMP软件手册目录的截图
张景中用了lisp，而另两人的工作似乎都是基于maple的 这是Java几何专家对勾股定理的“可读证明“，是很典型的面积消点法
http://hiphotos.baidu.com/%B0%D7%C0%CB/pic/item/9d2c3c6dfe257de5421694a4.jpg
[ 本帖最后由 wayne 于 2009-3-20 18:47 编辑 ] 更一般的结论：
如果一直线过Feuerbach点，分别与内切圆（或旁切圆）和九点圆交于P,Q，P关于三边切点构成的三角形DEF，Q关于三个中点构成的三角形MaMbMc，三个垂足HaHbHc构成的三角形的Simson直线与切点三角形的Euler直线平行，并且P关于切点三角形与Q关于中点三角形的Simson直线重合。 To wayne
我想，重要的有两点
1、如何表示命题，即定理的逻辑表示
2、如何运算
2是目前最难做的，也是最容易的
难在时间复杂度很大，容易在初学者即可写出暴力搜索算法
哈哈
当然，我等连初学者都不算
很有几种语言适合写这个东西
Maple算是其中不行的，lisp也失于繁琐
SML， Haskell都是比较合适的
回复 17# 无心人 的帖子
对于你的第二点，前面的三个人都做到了，%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
吴文俊的 "吴法"，(暗箱证明)
张景中的消点算法(可读证明)，杨璐的降维算法(二者均可) ，中国人应该感到自豪的：）
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
我真恨不得用那个Java几何砖家把楼主的题的证明展示一下，只是，只是我现在还不愿花时间使用这个软件，但从我在那网站的演示例子看的出来，Java几何专家完全能解决这个问题
回复 18# wayne 的帖子
15楼的图片：是勾股定理的机器可读证明： 自豪归自豪
但目前定理的机械证明还不能证明复杂的定理吧