Abstract
After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
D. Hilbert, Foundations of Geometry, Open Court Publishing Company, La Salla, Illinois, 1971.
W. T. Wu, Mathematics Mechanization, Science Press, Beijing, 2003.
A. Tarski, A Decision Method for Elementary Algebra and Geometry, The RAND Corporation Press, Santa Monica, 1948.
A. Seidenberg, A new decision method of elementary algebra, Annals of Mathematics, 1954, 60: 365–371.
G. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lecture Notes Computer Sciences 33, Springer-Verlag, Berlin, Heidelberg, 1975.
D. Arnon, Geometric reasoning with logic and algebra, Artificial Intelligence, 1988, 37: 37–60.
W. T. Wu, On the decision problem and the mechanization of theorem proving in elementary geometry, Journal of Systems Science and Mathematical Science, 1978, 21(16): 157–179 (in Chinese).
W. T. Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Science Press, Beijing, 1984 (in Chinese).
J. Ritt, Differential Algebra, American Mathematical Society, New York, 1950.
S. C. Chou, An introduction to Wu’s method for mechanical theorem proving in geometry, Journal of Automated Reasoning, 1988, 4: 237–267.
S. C. Chou, Proving Elementary Geometry Theorems Using Wu’s Algorithm, Automated Theorem Proving: After 25 Years (ed. by W. Bledsoe and D. Loveland), AMS Contemporary Mathematics Series, 1984, 29: 243–286.
S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.
B. Kutzler and S. Stifter, On the application of Buchberger’s algorithm to automated geometry theorem proving, Journal of Symbolic Computation, 1986, 2: 389–397.
B. Buchberger, G. Collins, and B. Kutzler, Algebraic methods for geometric reasoning, Annual Review of Computer Sciences, 1995, 3(19): 85–119.
D. Kapur, T. Saxena, and L. Yang, Algebraic and geometric reasoning with dixon resultants, Proceedings of International Symposium on Symbolic and Algebraic Computation (Oxford, 1994), ACM Press, New York, 1994 99–107.
J. Z. Zhang, L. Yang, and X. R. Hou, The sub-resultant method for automated theorem proving, Journal of Systems Science and Mathematical Sciences, 1995, 15(1): 10–15. (in Chinese).
D. M. Wang, Elimination procedures for mechanical theorem proving in geometry, Annals of Mathematics and Artificial Intelligence, 1995, 13: 1–24.
J. W. Hong, Can geometry be proved by an example? Scientia Sinica, 1986, 29: 824–834.
J. Z. Zhang and L. Yang, Principles of parallel numerical method and single-instance method of mechanical theorem proving, Mathematics in Practice and Theory, 1989, 1: 34–43.
J. Z. Zhang, L. Yang, and M. Deng, The parallel numerical method of mechanical theorem proving, Theoretical Computer Science, 1990, 74: 253–271.
H. Gelernter and N. Rochester, Intelligent behavior in problem-solving machines, IBM Journal, 1958: 336–345.
H. Gelernter, Realization of a Geometry Theorem Machine, Computers and Thought (ed. by E. Feigenbaum and J. Feldman), McGraw-Hill, New York, 1963.
H. Gelernter, J. Hansen, and D. Loveland, Empirical Explorations of the Geometry Theorem Proving Machine, Computers and Thought (ed. by E. Feigenbaum and J. Feldman), McGraw-Hill, New York, 1963.
S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated Production of Traditional Proofs for Theorems in Euclidean Geometry, IV, A Collection of 400 Geometry Theorems, TR-92-7, Department of Computer Science, WSU, 1992.
S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated production of traditional proofs for constructive geometry theorems, Proceedings of Eighth IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1993.
J. Z. Zhang, X. S. Gao, and S. C. Chou, The geometric information search system by forward reasoning, Chinese Journal of Computers, 1996, 19(10): 721–727 (in Chinese).
S. C. Chou, X. S. Gao, and J. Z. Zhang, A deductive database approach to automated geometry theorem proving and discovering, Journal of Automated Reasoning, 2000, 25(3): 219–246.
H. Goldstein, Elementary Geometry Theorem Proving, AIM-280, MIT, Cambridge, Massachusetts, 1973.
J. Anderson, C. Boyle, A. Corbett, and M. Lewis, The geometry tutor, Proceedings of IJCAI’85, Los Angles, 1985.
P. Gilmore, An examination of the geometry theorem proving machine, Artificial Intelligence, 1970, 1(2): 171–187.
A. Nevins, Plane geometry theorem proving using forward chaining, Artificial Intelligence, 1975, 6(1): 1–23.
S. Ullman, Model-Driven Geometry Theorem Prover, AIM-321, MIT, Cambridge, Massachusetts, 1975.
H. Coelho and L. Pereira, Automated reasoning in geometry theorem proving with prolog, Journal of Automated Reasoning, 1986, 2(4): 329–390.
T. Evans, A Heuristic Program to Solve Geometry Analogy Problems, Semantic Information Processing (ed. by M. Minsky), MIT Press, Cambridge, 1969.
J. Anderson, Tuning of Search of the Problem Space for Geometry Proofs, Proceeding of IJCAI’81, Vancouver, 1981.
Y. Zheng, S. C. Chou, and X. S. Gao, Visually dynamic presentation of proofs in plane geometry — part 2. Automated generation of visually dynamic presentation with the Full-Angle method and the deductive database method, Journal of Automated Reasoning, 2010, 45(3): 243–266
X. S. Gao, J. Z. Zhang, and S. C. Chou, Geometry Expert, Nine Chapters Publishing, TaiPei, Taiwan, 1998 (in Chinese).
J. G. Jiang and J. Z. Zhang, The automated geometry reasoning network based on equivalent class reasoning, Patttern Recognition and Artificial Intelligence, 2006, 19(5): 617–622 (in Chinese).
J. G. Jiang and J. Z. Zhang, The automated geometry reasoning system based on RETE algorithm, Journal of Sichuan University: Engineering Science Edition, 2006, 38(3): 135–139 (in Chinese).
J. G. Jiang, J. Z. Zhang, and X. J. Wang, Readable proving for a class of geometric theorems of polynomial equality type, Chinese Journal of Computers, 2008, 31(2): 207–213 (in Chinese).
R. Welham R, Geometry Problem Solving, D.A.I. Research Report No.14, 1976.
R. Wong, Construction Heuristics for Geometry and a Vector Algebra Representation of Geometry, Technical Memorandum 28, Project MAC, MIT, Cambridge, Massachusetts, 1973.
R. Reiter, A semantically guided deductive system for automatic theorem proving, IEEE Transactions on Computers, 1977, C-25(4): 328–334.
A. Robinson, Proving a theorem (as done by Man, Logician, or Machine), Automation of Reasoning (ed. by J. Siekmann and G. Wrightson), Springer-Verlag, Berlin, Heidelberg, 1983.
W. Elcock, Representation of knowledge in geometry machine, Machine Intelligence (ed. by W. Elcock and D. Michie), John Wiley and Sons, 1977, 8: 11–29.
G. Greeno, M. Magone, and S. Chaiklin, Theory of constructions and set in problem solving, Memory and Cognition, 1979, 7(6): 445–461.
N. Matsuda and K. Van Lehn, GRAMY: A geometry theorem prover capable of construction, Journal of Automated Reasoning, 2004. 32(1): 3–33.
J. McCharen, R. Overbeek, and L. Wos, Problems and experiments for and with automated theorem-proving programs, IEEE Transactions on Computers, 1976, C-25: 773–782.
A. Quaife, Automated Development of Tarski’s geometry, Journal of Automated Reasoning, 1989, 5: 97–118.
L. Meikle and J. Fleuriot, Formalizing Hilbert’s grundlagen in Isabelle/Isar, Theorem Proving in Higher Order Logics, 2003: 319–334.
P. Scott, Mechanizing Hilbert’s Foundations of Geometry in Isabelle, Master Thesis, School of Informatics, University of Edinburgh, 2008.
C. Dehlinger, J. Dufourd, and P. Schreck, Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry, Automated Deduction in Geometry (2000), LNAI 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001.
J. Narboux, A decision procedure for geometry in Coq, Proceedings of TPHOLs’ 2004, LNCS 3223 (ed. by S. Konrad, B. Annett, and G. Genesh), 2004.
J. Z. Zhang, S. C. Chou, and X. S. Gao, Automated production of traditional proofs for theorems in Euclidean geometry, I: The Hilbert intersection point theorems, Annals of Mathematics and Artificial Intelligence, 1995, 13: 109–137.
J. Narboux, A graphical user interface for formal proofs in geometry, Journal of Automated Reasoning, 2007, 39: 161–180.
R. Caferra, N. Peltier, and F. Puitg, Emphasizing human techniques in automated geometry theorem proving: A practical realization, Automated Deduction in Geometry (2000), LNAI 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001.
S. Fèvre, Integration of reasoning and algebraic calculus in geometry, Automated Deduction in Geometry (1996), Lecture Notes in Artificial Intelligence 1360, Springer-Verlag, Berlin, Heidelberg, 1998.
S. F`evre and D. M. Wang, Combining algebraic computing and term-rewriting for geometry theorem proving. Proceedings of AISC’98, Pittsburgh, USA, 1998.
G. Défourneaux, C. Bourely, and N. Peltier, Semantic generalizations for proving and disproving conjectures by analogy, Journal of Automated Reasoning, 1998, 20(1–2): 27–45.
S. C. Chou, X. S. Gao, and J. Z. Zhang, Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems, World Scientific, Singapore, 1994.
J. Z. Zhang, Points Elimination Methods for Geometric Problem Solving, Mathematics Mechanization and Applications (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000.
P. Janičić, J. Narboux, and P. Quaresma, The area method: A recapitulation, Journal of Automated Reasoning, 2012, 48(4): 489–532
J. Z. Zhang, How to Solve Geometry Problems Using Areas, Shanghai Educational Publishing Inc., Shanghai, 1982 (in Chinese).
J. Z. Zhang and P. Cao, From Education of Mathematics to Mathematics for Education, Sichun Educational Publishing Inc., Chengdu, 1988 (in Chinese).
J. Z. Zhang, A New Approach to Plane Geometry, Sichuan Educational Publishing Inc., Chengdu, 1992 (in Chinese).
S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated generation of readable proofs with geometric invariants, I: Multiple and shortest proofs generation, Journal of Automated Reasoning, 1996, 17(3): 325–347.
S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated generation of readable proofs with geometric invariants, II: Theorem proving with full-angles, Journal of Automated Reasoning, 1996, 17(3): 349–370.
S. C. Chou, X. S. Gao, and J. Z. Zhang, A Collection of 110 Geometry Theorems and Their Machine Proofs Based on Full-Angles, TR-94-4, Department of Computer Science, WSU, 1994.
Y. Zou and J. Z. Zhang, Automated generation of readable proofs for constructive geometry statements with the mass point method, Automated Deduction in Geometry (2010), Lecture Notes in Artificial Intelligence 6877, Springer-Verlag, Berlin Heidelberg, 2011.
S. C. Chou, X. S. Gao, and J. Z. Zhang, Mechanical geometry theorem proving by vector calculation, Proceedings of International Symposium on Symbolic and Algebraic Computation (Kiev, Ukraine, July 6–8, 1993), ACM Press, New York, 1993.
S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated production of traditional proofs in solid geometry, Journal of Automated Reasoning, 1995, 14: 257–291.
L. Yang, X. S. Gao, S. C. Chou, and J. Z. Zhang, Automated production of readable proofs for theorems in non-euclidean geometries, Automated Deduction in Geometry, Lecture Notes Computer Sciences 1360, Springer-Verlag, Berlin, Heidelberg, 1997.
H. B. Li, Clifford algebra approaches to mechanical geometry theorem proving, Mathematics Mechanization (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000.
B. Sturmfels, Computational algebraic geometry of projective configurations, Journal of Symbolic Computation, 1993, 11: 595–618.
J. Righter-Gebert, Mechanical theorem proving in projective geometry, Annals of Mathematics and Artificial Intelligence, 1995, 13: 139–172.
H. B. Li, New Explorations in Automated Theorem Proving in Geometries, Ph.D. Thesis, Peking University, China, 1994.
H. B. Li, Some applications of clifford algebra to geometries, Automated Deduction in Geometry (1989), Lecture Notes in Artificial Intelligence 1669, Springer-Verlag, Berlin, Heidelberg, 1998.
D. M. Wang, Clifford algebraic calculus for geometric reasoning with application to computer vision, Automated Deduction in Geometry (1996), Lecture Notes in Artificial Intelligence 1360, Springer-Verlag, Berlin, Heidelberg, 1998.
H. B. Li and H. Shi, On Erdös’ ten-point problem, Acta Mathematica Sinica, New Series, 1997, 13(2): 221–230.
S. Fèvre and D. M. Wang, Proving geometric theorems using clifford algebra and rewrite rules, Lecture Notes in Artificial Intelligence 1421 (ed. by D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 1997.
H. Q. Yang, S. G. Zhang, and G. C. Feng, A Clifford algebraic method for geometric reasoning, Automated Deduction in Geometry (Beijing, 1998), Lecture Notes in Artificial Intelligence 1669 (ed. by X. S. Gao, D. M. Wang, and L. Yang), Springer-Verlag, Berlin, Heidelberg, 1999.
H. B. Li, Vectorial equation-solving for mechanical geometry theorem proving, Journal of Automated Reasoning, 2000, 25: 83–121.
H. B. Li and M. Cheng, Clifford algebraic reduction method for automated theorem proving in differential geometries, Journal of Automated Reasoning, 1998, 21: 1–21.
H. B. Li, Mechanical theorem proving in differential geometry, Mathematics Mechanization (ed. by X. S. Gao and D. M. Wang), Academic Press, London, 2000.
A. Dolzmann, T. Sturm, and V. Weispfenning, A new approach for automatic theorem proving in real geometry, Journal of Automated Reasoning, 1998, 21(3): 357–380.
W. T. Wu, On problems involving inequalities, MM-Res, Preprints, MMRC, 1992, 7: 103–138.
W. T. Wu, On a finiteness theorem about problems involving inequalities, Journal of Systems Science and Mathematical Sciences, 1994, 7(2): 193–200.
D. M. Wang, Polynomial Equations Solving and Mechanical Geometric Theorem Proving, Ph.D. Thesis, Institute of Systems Science, Chinese Academy of Sciences, Beijing, 1993.
L. Yang, Recent advances in automated theorem proving on inequalities, Journal of Computer Science and Technology, 1999, 14(5): 434–446.
L. Yang, X. R. Hou, and B. C. Xia, A complete algorithm for automated discovering of a class of inequality-type theorems, Science in China (Series F), 2001, 44(1): 33–49.
L. Yang and J. Z. Zhang, A practical program of automated proving for a class of geometric inequalities, Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence 2061 (ed. by J. Richter-Gebert and D. M. Wang), Springer-Verlag, Berlin, Heidelberg, 2001.
O. Bottema, et al, Geometric Inequalities, Wolters-Noordhoff Publishing, Groningen, Netherlands, 1969.
L. Yang, Solving harder problems with lesser mathematics, Proceedings of the 10th Asian Technology Conference in Mathematics, ATCM Inc., Blacksburg, 2005.
L. Yang, Difference substitution and automated inequality proving, Journal of Guangzhou University: Natural Science Edition, 2006, 5(2): 1–7 (in Chinese).
L. Yang and Y. Yao, Difference substitution matrices and decision on nonnegativity of polynomials, Journal of Systems Science and Mathematical Sciences, 2009, 29(9): 1169–1177 (in Chinese).
Y. Yao, Infinite product convergence of column stochastic mean matrix and machine decision for positive semi-definite forms, Science China Mathematics (Series A), 2010, 53(3): 251–264 (in Chinese).
S. H. Xia, Automated Production of Readable Proof for a Class of Inequality-type Theorems, Ph.D, Thesis, Chinese Academy of Sciences, Beijing, 2002.
S. Chen and J. Z. Zhang, Automated production of elementary and readable proof of inequality, Journal of Sichuan University: Engineering Science Education, 2003, 35(4): 86–93 (in Chinese).
S. C. Chou, X. S. Gao, and J. Z. Zhang, Automated geometry theorem proving and geometry education, Proceedings of Asian Technology Conference in Mathematics, Association of Mathematics Educators, Singapore, 1995.
C. Z. Li and J. Z. Zhang, Readable machine solving in geometry and ICAI software MSG, Automated Deduction in Geometry (1998), Lecture Notes in Artificial Intelligence 1669, Springer-Verlag, Berlin, Heidelberg, 1998.
S. C. Chou, X. S. Gao, and J. Z. Zhang, An introduction to geometry expert, Proceedings of CADE-13, Lecture Notes in Artifficial Intelligence (ed. by M. McRobbie and J. Slaney), Springer-Verlag, Berlin, Heidelberg, 1996.
Y. Zheng, S. C. Chou, and X. S. Gao, An introduction to java geometry expert-(extended abstract), Automated Deduction in Geometry — 7th International Workshop (2008), LNCS 6301 (ed. by T. Sturm and C. Zengler), Springer, 2011.
Y. Zheng, S. C. Chou, and X. S. Gao, Visually dynamic presentation of proofs in plane geometry — part 1. Basic features and the manual input method, Journal of Automated Reasoning, 2010, 45(3): 213–241.
X. S. Gao, Q. Lin, MMP/Geometer-A software package for automated geometry reasoning, Automated Deduction in Geometry (Hagenberg Castle, Austria, 2002) (ed. by F. Winkler), Springer-Verlag, Berlin, Heidelberg, 2004: 44–66.
C. Z. Li and J. Z. Zhang, Super Sketchpad, Beijing Normal University Press, Beijing, 2004 (in Chinese).
S. Wilson and J. Fleuriot, Geometry explorer: combining dynamic geometry, automated geometry theorem proving and diagrammatic proofs, Proceedings of the 12th Workshop on Automated Reasoning (ARW), Edinburgh, UK, 2005.
P. Janicic and P. Quaresma, System description: GCLCprover + GeoThms, International Joint Conference on Automated Reasoning (IJCAR-2006), Lecture Notes in Artificial Intelligence 4130 (ed. by U. Furbach and N. Shankar), Springer-Verlag, Berlin, Heidelberg, 2006.
H. Zheng and J. Z. Zhang, Reasoning of algorithm of geometry automatic reasoning platform with sustainable development by user, Journal of Computer Applications, 2011, 31(8): 2101–2107 (in Chinese).
H. Zheng, The sustainable geometry automated reasoning platform, Journal of System Science and Mathematical Sciences, 2011, 31(12): 1622–1632 (in Chinese).
A. Samuel, Some studies in machine learning using the game of checkers, IBM Journal of Research and Development, 1959, 3(3): 210–229.
A. Samuel, Some studies in machine learning using the game of checkers II — Recent progress, IBM Journal of Research and Development, 1967, 11(6): 601–617.
Author information
Authors and Affiliations
Corresponding author
Additional information
This research was supported by the Funds of the Chinese Academy of Sciences for Key Topics in Innovation Engineering under Grant No. KJCX2-YW-S02.
This paper was recommended for publication by Editor Xiao-Shan GAO.
Rights and permissions
About this article
Cite this article
Jiang, J., Zhang, J. A review and prospect of readable machine proofs for geometry theorems. J Syst Sci Complex 25, 802–820 (2012). https://doi.org/10.1007/s11424-012-2048-3
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11424-012-2048-3