×

zbMATH — the first resource for mathematics

Generalizing Morley’s and other theorems with automated realization. (English) Zbl 1398.68480
Summary: A new approach is shown that mechanically proves various theorems in plane geometry by recasting them in terms of constraint satisfaction. A Python 3 implementation called GEOPAR affords transparent proofs of well-known theorems as well as new ones, including a generalization of Morley’s Theorem.
MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51M04 Elementary problems in Euclidean geometries
Software:
GEOPAR; GitHub; Python
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994) · Zbl 0941.68503
[2] Chou, S-C; Gao, X-S; Zhang, J-Z, Automated generation of readable proofs with geometric invariants, J. Autom. Reason., 17, 349, (1996) · Zbl 0865.68110
[3] Connes, A, A new proof of morley’s theorem, Pub. Math. de l’IHÉS, 88, 43-46, (1998) · Zbl 1006.51010
[4] Conway, J; Blackwell, A (ed.); Mackay, D (ed.), The power of mathematics, (2005), Cambridge
[5] Conway, J.: in Euclidean Geometry Proofs in THE BOOK. http://mathforum.org/kb/thread.jspa?messageID=1382215&tstart=0. Accessed 27 July 2015
[6] Dijkstra, E.W.: Selected Writings on Computing: A Personal Perspective. Springer, New York (1982) · Zbl 0497.68001
[7] Dijkstra, E.W.: On the design of a simple proof for Morley’s theorem, EWD 1050. https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1050.html. Accessed 27 July 2015 · Zbl 0406.01008
[8] Dijkstra, E.W.: Proving an implication via its converse, EWD 1266a. https://www.cs.utexas.edu/users/EWD/ewd12xx/EWD1266a.PDF. Accessed 27 July 2015 · Zbl 1006.51010
[9] Janičić, P; Narboux, J; Quaresma, P, The area method a recapitulation, J. Autom. Reason., 48, 489-532, (2012) · Zbl 1242.68281
[10] Oakley, CO; Baker, JC, The Morley trisector theorem, Am. Math. Mon., 85, 737-745, (1978) · Zbl 0406.01008
[11] Okabe, A., Boots, B., Sugihara, K., Chiu, S.N.: Spatial Tessellations: Concepts and Applications of Voronoi Diagrams, 2nd edn. Wiley, Hoboken (2000) · Zbl 0946.68144
[12] Stonebridge, B, A simple geometric proof of morley’s trisector theorem, Mathematical Spectrum, 42, 1, (2009)
[13] Wu, WT, Basic principles of mechanical theorem proving in elementary geometries, J. Autom. Reason., 2, 3, (1986) · Zbl 0642.68163
[14] Wu, W.T.: Mathematics Mechanization: Mechanical Geometry Theorem-Proving. Mechanical Geometry Problem-Solving and Polynomial Equations-Solving. Springer, New York (2001) · Zbl 0987.68074
[15] https://github.com/ebraude/geopar
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.