×

Morley’s theorem revisited: origami construction and automated proof. (English) Zbl 1211.51011

Summary: 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.

MSC:

51M15 Geometric constructions in real or complex geometry
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)

Software:

Epsilon
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Alperin, R. C., A mathematical theory of origami constructions and numbers, New York Journal of Mathematics, 6, 119-133 (2000) · Zbl 1065.51501
[2] Alperin, R. C.; Lang, R. J., One-, two, and multi-fold origami axioms, \((Origami^4\): 4th International Meeting of Origami Science, Mathematics and Education, 4OSME 2006 (2009), A K Peters Ltd.), 371-393
[3] Bogomolny, A., 1996. Morley’s Miracle. URL: http://www.cut-the-knot.org/triangle/Morley; Bogomolny, A., 1996. Morley’s Miracle. URL: http://www.cut-the-knot.org/triangle/Morley
[4] Buchberger, B., Groebner-bases: an algorithmic method in polynomial ideal theory, (Bose, N., Multidimensional Systems Theory — Progress, Directions and Open Problems in Multidimensional Systems (1985)), Copyright: Reidel Publishing Company, Dordrecht, Boston, Lancaster, The Netherlands, Ch. 6, pp. 184-232, (Second edition: Bose N.K. (Ed.): Multidimensional Systems Theory and Application, Kluwer Academic Publisher, 2003, pp. 89-128) · Zbl 0587.13009
[5] Buchberger, B., Algorithm supported mathematical theory exploration: a personal view and strategy, (Campbell, J., Proceedings of 7th International Conference on Artificial Intelligence and Symbolic Computation. Proceedings of 7th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2004. Proceedings of 7th International Conference on Artificial Intelligence and Symbolic Computation. Proceedings of 7th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2004, Lecture Notes in Artificial Intelligence, vol. 3249 (2004), Springer), 236-250 · Zbl 1109.68664
[6] Collart, S.; Kalkbrener, M.; Mall, D., Converting bases with the Gröbner walk, Journal of Symbolic Computation, 24, 3-4, 465-469 (1997) · Zbl 0908.13020
[7] Fushimi, K., October 1980. Science of origami. A supplement to Saiensu (in Japanese).; Fushimi, K., October 1980. Science of origami. A supplement to Saiensu (in Japanese).
[8] Geretschläger, R., Geometric Constructions in Origami (2002), Morikita Publishing Co., (in Japanese), translation by Hidetoshi Fukagawa
[9] Ghourabi, F.; Ida, T.; Takahashi, H.; Marin, M.; Kasem, A., Logical and algebraic view of Huzita’s origami axioms with applications to computational origami, (Proceedings of the 22nd ACM Symposium on Applied Computing (2007), ACM Press), 767-772
[10] Hatori, K., 2005. K’s origami - fractional library - origami construction. URL: http://origami.ousaan.com/library/conste.html; Hatori, K., 2005. K’s origami - fractional library - origami construction. URL: http://origami.ousaan.com/library/conste.html
[11] Huzita, H., 1989. Axiomatic development of origami geometry. In: Proceedings of the First International Meeting of Origami Science and Technology. pp. 143-158.; Huzita, H., 1989. Axiomatic development of origami geometry. In: Proceedings of the First International Meeting of Origami Science and Technology. pp. 143-158.
[12] Ida, T.; Buchberger, B., Proving and solving in computational origami, (Analele Universitatii de Vest din Timisoara. Analele Universitatii de Vest din Timisoara, Fasc. Special of Mathematica-Informatica, vol. XLI (2003)), 247-263 · Zbl 1073.68816
[13] Ida, T.; Marin, M.; Takahashi, H.; Ghourabi, F., Computational origami construction as constraint solving and rewriting, (16th International Workshop on Functional and (Constraint) Logic Programming. 16th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2007. 16th International Workshop on Functional and (Constraint) Logic Programming. 16th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2007, Electronic Notes in Theoretical Computer Science (2007), R. Echahed), 139-152
[14] Ida, T., Takahashi, H., Ţepeneu, D., Marin, M., 2005. Morley’s theorem revisited through computational origami. In: Proceedings of the 7th International Mathematica Symposium, IMS 2005.; Ida, T., Takahashi, H., Ţepeneu, D., Marin, M., 2005. Morley’s theorem revisited through computational origami. In: Proceedings of the 7th International Mathematica Symposium, IMS 2005.
[15] Ida, T.; Takahashi, H.; Marin, M.; Ghourabi, F.; Kasem, A., Computational construction of a maximal equilateral triangle inscribed in an origami, (Mathematical Software, ICMS 2006. Mathematical Software, ICMS 2006, Lecture Notes in Computer Science, vol. 4151 (2006), Springer), 361-372 · Zbl 1230.51023
[16] (Jones, A.; Morris, S. A.; Pearson, K. R., Abstract Algebra and Famous Impossibilities (1994), Springer-Verlag) · Zbl 0758.12001
[17] Wang, D., Elimination Practice: Software Tools and Applications (2004), Imperial College Press: Imperial College Press London · Zbl 1099.13047
[18] Wang, D., 2008. Personal communication.; Wang, D., 2008. Personal communication.
[19] Wantzel, M., Recherches sur les moyens de reconnaître si un Problème de Géométrie peut se résoudre avec la règle et le compas, Journal de Mathématiques Pures et Appliquées, 1, 2, 366-372 (1837)
[20] Wu, W., Basic principles of mechanical theorem proving in elementary geometry, Journal of Automated Reasoning, 2, 221-252 (1986) · Zbl 0642.68163
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.