Morley's theorem revisited: Origami construction and automated proof
Morley's theorem revisited: Origami construction and automated proof
复制标题
DOI：
10.1016/j.jsc.2010.10.007
复制
发表时间：
2011-05
期刊：
影响因子：
--
通讯作者：
T. Ida;Asem Kasem;Fadoua Ghourabi;Hidekazu Takahashi
中科院分区：
文献类型：
--
作者：
T. Ida;Asem Kasem;Fadoua Ghourabi;Hidekazu Takahashi
莫利定理指出，对于任何三角形，其相邻角三等分线的交点形成等边三角形。由于众所周知的角三等分的不可能性结果，用直尺和圆规方法构造莫利三角形是不可能的。然而，通过折纸，可以构造三等分角，因此也可以构造莫利三角形。在本文中，我们提出了莫利三角形的计算折纸构造以及广义莫利定理的自动正确性证明。在计算折纸构造过程中，生成并累积符号表示中的几何约束。然后，这些约束被转换为代数形式，即一组多项式，进而用于证明构造的正确性。自动证明基于 Gröbner 基础方法。给出了用于证明的 Gröbner 基础计算的实验时间。它们根据折纸构造方法、Gröbner 基础计算算法和变量排序而有很大差异。
Morley’s theorem states that for any triangle, the intersections of its adjacent angle trisectors form an equilateral triangle. The construction of Morley’s triangle by the straightedge and compass method is impossible because of the well-known impossibility result for angle trisection. However, by origami, the construction of an angle trisector is possible, and hence that of Morley’s triangle. In this paper we present a computational origami construction of Morley’s triangle and an automated correctness proof of the generalized Morley’s theorem. During the computational origami construction, geometrical constraints in symbolic representation are generated and accumulated. Those constraints are then transformed into algebraic forms, i.e. a set of polynomials, which in turn are used to prove the correctness of the construction. The automated proof is based on the Gröbner bases method. The timings of the experiments of the Gröbner bases computations for our proofs are given. They vary greatly depending on the origami construction methods, the algorithms for the Gröbner bases computation, and variable orderings.