《几何专家》无法求解的问题

Ysu2008

如图，已知三角形ABC中，BD＝CE＝AF，且三角形DEF是正三角形，求证：三角形ABC也是正三角形。


上面这道题就无法用目前的推理软件求解，原因在于：
用《几何专家》求解，需要将几何图形各个约束关系和条件准确无误地输入计算机，也就是要将待求解的几何图形在满足题设要求的条件下画出来。

上面这道题，作图时，是先将三角形ABC画作正三角形（这是待证明的），再作BD＝CE＝AF，三角形DEF自然是正三角形。就是说画图顺序与证明顺序刚好相反。且，我们还不能先画三角形DEF。如果先画正三角形DEF，我们无法将三角形ABC用作图的方式“约束”为一个正三角形。

人类可以假装不知道三角形ABC是正三角形，但计算机就不行了。这道题输入计算机要求证明三角形ABC是正三角形，机器的证明只能是：因为三角形ABC是正三角形（我们就是这么输入的），所以它是正三角形。这就尴尬了。

ataorj

怎么做图的，它不应该追踪，它掌握着全局，还要它破什么案？
应该这样才合理:
告知局部，推测全貌及扩展结论。

Ysu2008

《几何专家》下载地址：
http://www.cs.wichita.edu/~ye/download.html

这是原版，是免费软件。该软件需要Java运行环境(JRE)，如果你的计算机从未安装过Java，也可以下载安装该网页提供的JRE版本。
(1)解压几何专家zip压缩包;
(2)安装JRE;
(3)双击 jgex.jar 文件。界面可设置为中文。

ataorj

超级画板也有推理能量，它们相比较如何？
它们我都没用过。

ccmmjj

这个问题我早已解决。请参看http://www.mathchina.com/bbs/for ... id=39243&extra=

Ysu2008

ccmmjj 发表于 2018-12-5 12:25
这个问题我早已解决。请参看http://www.mathchina.com/bbs/forum.php?mod=viewthread&tid=39243&extra=

我知道，我是想看看有没有别的路子。

Ysu2008

ataorj 发表于 2018-12-5 11:52
超级画板也有推理能量，它们相比较如何？
它们我都没用过。

没有用过超级画板。