用于解决几何查询的软件程序

当我利用在高中的奥林匹克竞赛中完成比赛时,我们称之为几何形状的庆祝活动可以理解各种不那么复杂的几何问题。 首先,您肯定会使用变量对布局中的每个角度进行分类,然后使用最小的标准几何过程集来定位组件之间的关系,删除公式,然后在某些时候获得结果。 感觉就像你可以编程计算机系统的例子。 所以,我很感兴趣,是否有任何类型的软件程序可以做到这一点? 我认识到有很多软件程序用于解决公式问题,但是存在什么东西可以让你实际输入几何问题而不用手工转换成公式? 我也没有寻求任何进展,也只是看到一个努力肯定是有趣的。 如果有任何合适的东西,我认为肯定会有兴趣在众多竞争对手中运行结果,并且还会看到它所解决的查询量。

0
2019-05-04 18:38:02
资源 分享
答案: 2

您可能对Doron Zeilberger的互联网网站感到好奇。 他实际上有一个合格的网页“平面几何:初级教科书(大约2050年)”,在那里他描绘了一个地球仪,计算机系统可以在没有人为治疗或干扰的情况下获得每一个飞机的几何形状。 随着Maple计划的到来证实了计算机系统的几个声明。

该网页存在于http://www.math.rutgers.edu/~zeilberg/PG/gt.html

0
2019-05-08 18:13:44
资源

这只是计算机化理论确认的祖父条款。 一个奇妙的观点是一些几何问题毫无疑问可以通过算法解决。

有概念表明这种系统可以通过算法来理解。 我不认识是否有人实际创建了程序来执行此操作。 JGEX似乎这样做。

张敬忠在中国推广了机械几何证据策略。 他首先将其作为设备的一种手段来解决连接位置,大小或角度之间百分比的几何问题。 在那之后,我认识的一些奥林匹克运动员开始利用它来抨击那种麻烦。 我不清楚这个名字在英语中是什么,但该方法的实际翻译是“因子消除方法”。 虽然它并不特别像你所说的那样,但由于“输入几何故障”需要你从直边和指南针给建筑和施工带来麻烦,这实际上就像“手工改造”公式“。

主题演讲:

  1. 用罗盘和直尺构建初始故障,按建筑和施工顺序制作每个创建因子的清单,允许它记录在每个因素的建立和建设中使用哪些因素。 (在替换动作3和4中都只使用了构造因子P的因子)

  2. 将理论转化为同等的理论。 通常a / b = 1,其中a和b也是大小的特征以及特定扇区或三角形的位置。 允许称这个公式为E.

  3. 设P是L的最后一个因子。对于E中出现的每个P,用L中的各种其他因子替换它(另外允许P本身),通常如果我们确认有关尺寸,我们可以做使用位置。 该行动需要一份可行程序清单。 当程序确定使用各种替换时,它可以作为证据树分支。

  4. 做一个去除因子P的额外替换。例如,如果在过去的动作中,我们将大小替换为位置,之后我们打算找到需要大小的东西。

  5. 做3到4结束,直到我们有1 = 1

一个实例:

角平分理论

给定:$AD$是三角形$\triangle ABC$的$\angle BAC$的角平分线。 允许$XYZ$是三角形$\triangle XYZ$的位置,$XY$也是扇区$XY$的大小。

确认:$\frac{AB}{AC} = \frac{BD}{DC}$

证明:

  1. 首先构造$ABC$。 之后构造$AD$。 清单$L$中的因子是$A,B,C,D$。

  2. 理论的平等公式是$\frac{AB}{AC} \frac{DC}{BD} = 1$

  3. $\frac{AB}{AC} \frac{DC}{BD} = \frac{AB}{AC} \frac{ACD}{ABD}$(替换大小与位置)

  4. $=\frac{AB}{AC} \frac{\frac{1}{2} AC\cdot AD \sin \angle CAD}{\frac{1}{2} AB\cdot AD \sin \angle BAD}$,此操作通过终止有效地删除因子$D$。

  5. $=\frac{AB}{AC} \frac{AC}{AB} =1$

这只是对这种计算机化系统如何运作的非官方描述。 我认为坚持张的出版肯定会告诉你额外的关于它:几何中的机器证据:几何理论的清晰计算机制造。 我没有阅读指南,但它的总结感觉就像你在寻找。 张和他的同事的几篇论文可以位于JGEX的互联网站点。 关于它的JGEX文档的自动化定理证明也是一个很好的来源。

0
2019-05-08 06:54:37
资源