一条很难用公理证明的几何新定理？

wayne

你是说 涉及到了自然语言的谓词处理吧，可我好像记得我们中国的吴文俊之 “吴氏消元法”可以办到，.....

无心人

那倒不是

应该是属于 数理逻辑 吧
ML程序设计语言是较少的讲这个的程序设计的书

wayne

今天在图书馆看了两本几何定理机器证明的书，以前的模糊得到了澄清。

说到几何定理机器证明，其实应该提到三个人，吴文俊，张景中，杨璐。

吴文俊的证明，核心是"吴法"，但最终返回的结果是命题的真与假，至于中间过程具体是怎样的，被软件处理成了黑箱子，我们无从知晓。
而张景中的是改进版的，核心是消点算法，是可读证明。

前面二人的方法只能证明等式的命题，而杨璐的降维算法可以证明不等式，其应用领域也由几何扩充到代数了。

wayne

原帖由 wayne 于 2009-3-20 12:03 发表
你是说 涉及到了自然语言的谓词处理吧，可我好像记得我们中国的吴文俊之 “吴氏消元法”可以办到，.....

自然语言处理这部分，我当时没搞清楚，说的有点问题。
下面是MMP软件手册目录的截图

张景中用了lisp，而另两人的工作似乎都是基于maple的

wayne

这是Java几何专家对勾股定理的“可读证明“，是很典型的面积消点法


[ 本帖最后由 wayne 于 2009-3-20 18:47 编辑 ]

dlsh

更一般的结论：
      如果一直线过Feuerbach点，分别与内切圆（或旁切圆）和九点圆交于P,Q，P关于三边切点构成的三角形DEF，Q关于三个中点构成的三角形MaMbMc，三个垂足HaHbHc构成的三角形的Simson直线与切点三角形的Euler直线平行，并且P关于切点三角形与Q关于中点三角形的Simson直线重合。

无心人

To wayne
    我想，重要的有两点
    1、如何表示命题，即定理的逻辑表示
    2、如何运算

2是目前最难做的，也是最容易的
难在时间复杂度很大，容易在初学者即可写出暴力搜索算法

哈哈
当然，我等连初学者都不算

很有几种语言适合写这个东西
Maple算是其中不行的，lisp也失于繁琐
SML， Haskell都是比较合适的

wayne

对于你的第二点，前面的三个人都做到了，
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
吴文俊的 "吴法"，(暗箱证明)
张景中的消点算法(可读证明)，杨璐的降维算法(二者均可) ，中国人应该感到自豪的：）
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

我真恨不得用那个Java几何砖家把楼主的题的证明展示一下，只是，只是我现在还不愿花时间使用这个软件，但从我在那网站的演示例子看的出来，Java几何专家完全能解决这个问题

wayne

15楼的图片：
是勾股定理的机器可读证明：

无心人

自豪归自豪

但目前定理的机械证明还不能证明复杂的定理吧