查看论文：http://preprint.nstl.gov.cn/newprint...=1142671836850

已经获准参加国际会议
Dear ADG contributor: it is my pleasure to inform you that the PC
Committee has decided to accept your contribution. Attached please
find the referees' reports.

As described in the call for papers (see
http://webs.uvigo.es/adg2006/cfp.html ), all accepted contributions
will be published as an internal working document that will be handled
to the participants at the meeting.

For this purpose we urge you to

-revise your contribution according to the referees' suggestions

-follow strictly the guidelines for publication as established in
http://webs.uvigo.es/adg2006/cfp.html , ie. follow the standard
Springer Proceedings format (llncs2e.cls, etc.).

This is crucial for the coherence of the internal working document
(page numbers, author index, style, etc). we have referred to.

NO Word files, etc., please.

-send your revised and formatted file (SOURCE file and EPS of figures)
to adg2006#@uvigo.es before JUNE 30.


Do not forget to register in ADG and to take care of your hotel
reservation (as soon as possible: there is a deadline for a number of
rooms pre-reserved for the ADG), see

http://webs.uvigo.es/adg2006/index.html


Thanks again.

See you in Pontevedra.

Tomas Recio

中国科学院研究员的意见

离开会还有较长时间，请对您的工作的“机器实现算法”，和与其他可读证明算法的比较，进行完善（如没有则努力完成之）。

我没有选择审理您的报告（需要避嫌）。从三位审理意见，您的工作得到很好的评价。

只有在以上两个问题上有清楚的工作，您的贡献才能被正确评价。


另：他们询问你的通信地址，请及时告知。如你有财力困难，可以向他们申请免除注册费。

请求高手们指导应该如何写出下面问题的算法？已经编写出Mathematica程序，为什么专家们还要求写算法？证明思路就应该是算法吗？

EB、EC分别交圆O于AD，AC、BD交于G，AD、BC交于F，求证：OG垂直EF。

思路：任意选定圆上四点Ａ，Ｂ，Ｃ，Ｄ，用交点公式表示出E,F,G,按照条件证明即可
证明：设原点通过圆心，圆O是单位圆，可以写出Mathematica程序：

高手们：距离开会只有约两个月时间，还有许多工作要做，恳求帮忙！非常感谢！

更多问题证明的Mathematica程序请参考：
http://www.channelwest.com/bbs/showt...34&Forum_ID=10

你是在搞平面几何定理的机器证明么？

嗯嗯，这个方向我基本上是一窍不通，但是看着你的问题还是感觉非常奇怪：搞平面几何定理的机器证明，不就是设计一个可以机械化地证明平面几何定理的算法么？这个应该是你论文的核心内容才对呀？更奇怪的是，你为什么要求一个能够证明那条定理的算法呢？针对一条特定定理的证明算法和平面几何定理的机器证明完全是两回事啊？

解释一下吧。另外最好把你 submission 到 ADG 的论文张贴一下，如果方便的话，能给出 reviewer 的 comment 是最好了。

虽然看不懂你想干什么， 但是看到久违的mathmatic还是眼前一亮……

怎么没动静了？

由于忙于按照标准格式重新排版论文，一直没有来这里，十分抱歉！感谢各位关注！

搞平面几何定理的机器证明，不就是设计一个可以机械化地证明平面几何定理的算法么？这个应该是你论文的核心内容才对呀？？
平面几何定理的机器证明的基础还是数学理论。吴文俊的方法公认为是这个领域的里程碑，其本质是提出一种新的理论，但是，人很难读懂，也就是可读性差，这也是公认的。张景中院士提出的面积方法，可读性好，但是对一些难题很难证明。我提出的方法，请参考外国专家的评论。虽然我的论文核心内容不是机器证明的算法，由于提出可以应用于机器证明的新的数学理论，所以入选，也属于会议要求的范围。

更奇怪的是，你为什么要求一个能够证明那条定理的算法呢？针对一条特定定理的证明算法和平面几何定理的机器证明完全是两回事啊？
请问：可以写出几何定理的机器证明的通用算法吗？
长远目标是编写出程序，但是现在我只会针对具体问题写出Mathematica程序，因此，希望高手指导。



评论：
Paper Info
----------
Paper ID : 14
Paper Title : The technique for conjugate ratio for geometric theorem proving

Evaluation
----------
Use the following scheme:
Y = Yes, acceptable
N = No, not acceptable.

Scope : Y
Originality : Y
Presentation : Y

Overall : Y

Comments to the author
=================================================
Paper Info
----------
Paper ID: 14
Paper Title: The Technique of Conjugate Ratio for Geometric Theorem Proving

Evaluation
----------
Use the following scheme:
Y = Yes, acceptable
N = No, not acceptable.

Scope: Y
Originality: Y
Presentation: Y

Overall: Y

Comments to the author
----------------------

This is an interesting approach to GTP based on complex numbers. The description of the technique is clear and readable, with plenty of worked-out examples. It would be nice if the author could give an idea of the number of examples that have been proved with this approach along with timings (to enable us to gauge its efficiency, for instance). Also, there should be some (more detailed) comparison of the relative merits of this method with respect to other approaches, especially those that can produce readable proofs of similar results. The longer term plans for this project, if any, should be outlined.

======================================================


Paper Info
----------
Paper ID : 14
Paper Title : The Technique of Conjugate Ratio
for Geometric Theorem Proving

Evaluation
----------
Use the following scheme:
Y = Yes, acceptable
N = No, not acceptable.

Scope : Y-
Originality : Y-
Presentation : Y
Overall : Y

Comments to the author
----------------------

The proposed talk will demonstrate how to exploit the use of complex
numbers in automatic theorem proving. For this the author first sets up
several geometric primitive operations, like angle measurement, co-linearity, co-circularity, etc. and expresses these primitives as relations between
suitably chosen complex parameters. Here in particular the use of complex
conjugates is important to derive as relatively simple ratio formulas.
Later in the extended abstract it is shown how these complex expressions
can be used to derive relatively simple proofs of planar geometric theorems
involving circles, points and lines.

For me it is not clear how the proposed formulas can be used to automatically
deduce proofs for geometric theorems, since the author does not provide any
algorithmic methods how the primitive formulae are combined. Still he presents
a few nice examples where with his parameterizations nice proofs for geometric
theorems can be written. It is not clear, wheter these proves were found by hand
or automatically. One of the examples makes use of Mathematica, but there only
the "Solve" and "Simplify" routines were used.

Still I recommend the paper for presentation at the ADG, since at least nice
algebraic approaches are presented. It would be nice to see how these approaches
can be used in an automatic deduction system.



=========================================================

Paper Info
----------
Paper ID :
Paper Title : Technique of Conjugate Ratio for Geometric Theorem Proving

Evaluation
----------
Use the following scheme:
Y = Yes, acceptable
N = No, not acceptable.

Scope : Y
Originality : Y
Presentation : Y

Overall : marginal

Comments to the author
----------------------

The paper discusses the use of vector ration and conjugate
ratio for geometry theorem proving.

I liked the content of the paper very much.

I would have liked to see the comparison of the proposed
approach with the vector method, area method and other related method.

The abstract claims that the method generates readable proofs. I did not
see any evidence of that in the paper. Perhaps the presentation can focus
on that issue.

请参考附件。

上传的附件

共轭比论文.pdf.pdf (234.5 KB, 10 次查看)

你好，你的论文我大致看过了，感觉不是特别清楚，所以还得再多问两句。

首先你是搞了一种利用复数和向量来证明平面几何定理的方法对吧？我想问的就是，你这个方法是“机械”的吗？从你的论文中我没有看出这一点来。就我所知，几何定理的机器证明，最重要的就是要能够得出一个能够证明定理的“机械”算法。简单一点来说，就是你可以写出一个程序，把任意一个几何定理按照一定的格式输入进去，然后这个程序就能够在无需人干预的情况下对这个定理进行证明 —— 当然有可能某些定理这个程序证不出来，不过这个是方法优劣的问题了。

所以我想问问你，你这个方法是“机械”的吗？从你的论文里面，似乎没有体现这一点，那些定理的证明都是针对一个具体的问题，你自己根据定理的情况应用了一些公式，然后得到一个证明。这当然很好，但是这似乎仍然是传统的人工证明定理的做法，你能让计算机来替你选择应该应用哪些公式，然后得出一个证明吗？

另，你的这篇论文读起来不太顺，有些符号和概念似乎未加定义就使用了，我想这应该是草稿吧？一般来说，ADG 这类国际会议是不收中文论文的，你能把你投递到 ADG 的英文正式版本张贴一下吗？

盼复。

文中的方法只是为机器证明提供一种理论，当然，不是机械的。下一个目标就是用这种理论编自动证明的程序。
无法上传附加，请到邮箱查收。

请提供邮箱。

这样啊，那可能有点麻烦了。

我也觉得你的论文里的想法不错，能够做出来的话，或许是很漂亮的。但是如果当前你的方法仍然不是机械的，还是需要依赖于人工证明的话，那后面的工作还有很多，而且是远非平凡的。也就是说，在某种意义上，你的工作仍然处于半成品状态。

我自己并不是特别熟悉这个方向，而且最近也比较忙，恐怕无法帮助你完成这个工作，特别是你的时间只有两个月。或许你可以去找一个这个方向的老师或研究生请求合作，国内这个方向还是有一些较强的研究者的，相信你也知道。不过这样一来，你可能就要与其他人分享你的成果了。

如果你愿意，也可以把论文发给我，我会看看周围有没有合适的人选。我的电子邮件：
xie_zhiyi (at) fudan.edu.cn