Automated production of readable proofs for theorems in non-Euclidean geometries

  • Lu Yang
  • Xiao-Shan Gao
  • Shang-Ching Chou
  • Jing-Zhong Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1360)


We present a complete method which can be used to produce short and human readable proofs for a class of constructive geometry statements in non-Euclidean geometries. The method is a substantial extension of the area method for Euclidean geometry. The method is an elimination algorithm which is similar to the variable elimination method of Wu used for proving geometry theorems. The difference is that instead of eliminating coordinates of points from general algebraic expressions, our method eliminates points from high level geometry invariants. As a result the proofs produced by our method are generally short and each step of the elimination has clear geometric meaning. A computer program based on this method has been used to prove more than 90 theorems from non-Euclidean geometries including many new ones. The proofs produced by the program are generally very short and readable.


Theorem Prove Elliptic Geometry Hyperbolic Geometry Geometric Quantity Automate Theorem Prove 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S. C. Chou, Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.Google Scholar
  2. 2.
    S. C. Chou, X. S. Gao, & J. Z. Zhang, Machine Proofs in Geometry, World Scientific Pub., Singapore, 1994.Google Scholar
  3. 3.
    S. C. Chou & X. S. Gao, Mechanical Theorem Proving in Riemann Geometry, Computer Mathematics, W. T. Wu ed., World Scientific Pub., Singapore, pp. 136–157, 1993.Google Scholar
  4. 4.
    S. C. Chou, X. S. Gao, L. Yang, & J. Z. Zhang, Automated Production of Readable Proofs for Theorems in non-Euclidean Geometries, TR-WSU-94-9, 1994.Google Scholar
  5. 5.
    S. C. Chou, X. S. Gao, L. Yang, & J. Z. Zhang, A Collection of 90 Automatically Proved Geometry Theorems in non-Euclidean Geometries, TR-WSU-94-10, 1994.Google Scholar
  6. 6.
    H. Coelho & L. M. Pereira, Automated Reasoning in Geometry with Prolog, J. of Automated Reasoning, 2, 329–390, 1987.CrossRefGoogle Scholar
  7. 7.
    H. S. M. Coxeter, Non-Euclidean Geometry, Univ. of Toronto Press, 1968.Google Scholar
  8. 8.
    X. S. Gao, Transcendental Functions and Mechanical Theorem Proving in Elementary Geometries, J. of Automated Reasoning, 6, 403–417, 1990.Google Scholar
  9. 9.
    H. Gelernter, J. R. Hanson, & D. W. Loveland, Empirical Explorations of the Geometry-theorem Proving Machine, Proc. West. Joint Computer Conf., pp. 143–147, 1960.Google Scholar
  10. 10.
    M. J. Greenberg, Euclidean Geometry and non-Euclidean Geometry, Development and History, Freeman, 1980.Google Scholar
  11. 11.
    B. Grünbaum & G. C. Shephard, From Mennelaus to Computer Assisted Proofs in Geometry, Preprint, Washington State University, 1993.Google Scholar
  12. 12.
    T. Havel, Some Examples of the Use of Distances as Coordinates for Euclidean Geometry, J. of Symbolic Computation, 11, 579–594, 1991.Google Scholar
  13. 13.
    K. R. Koedinger & J. R. Anderson, Abstract Planning and Perceptual Chunks: Elements of Expertise in Geometry, Cognitive Science, 14, 511–550, 1990.CrossRefGoogle Scholar
  14. 14.
    A. J. Nevins, Plane Geometry Theorem Proving Using Forward Chaining, Artificial Intelligence, 6, 1–23, 1976.CrossRefGoogle Scholar
  15. 15.
    D. Kapur, Geometry Theorem Proving Using Hilbert's Nullstellensatz, Proc. of SYMSAC'86, Waterloo, pp. 202–208, 1986.Google Scholar
  16. 16.
    B. Kutzler & S. Stifter, A Geometry Theorem Prover Based on Buchberger's Algorithm, Proc. CADS-7, Oxford, ed. J. H. Siekmann, LNCS, no. 230, pp. 693–694, 1987.Google Scholar
  17. 17.
    S. Stifter, Geometry Theorem Proving in Vector Spaces by Means of Gröbner Bases, Proc. of ISSAC-98, Kiev, ACM Press, pp. 301–310,1993.Google Scholar
  18. 18.
    T. E. Stokes, On the Algebraic and Algorithmic Properties of Some Generalized Algebras, Ph.D thesis, University of Tasmania, 1990.Google Scholar
  19. 19.
    A. Tarski, A Decision Method for Elementary Algebra and Geometry, Univ. of California Press, Berkeley, 1951.Google Scholar
  20. 20.
    D. M. Wang, On Wu's Method for Proving Constructive Geometry Theorems, Proc. IJCAI'89, Detroit, pp. 419–424, 1989.Google Scholar
  21. 21.
    D. M. Wang, Elimination Procedures for Mechanical Theorem Proving in Geometry, Ann. of Math. and AI, 13, 1–24, 1995.Google Scholar
  22. 22.
    W. T. Wu, On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry, Scientia Sinica 21, 159–172, 1978, Also in Automated Theorem Proving: After 25 years, A.M.S., Contemporary Mathematics, 29, pp. 213-234, 1984.Google Scholar
  23. 23.
    W. T. Wu, Basic Principles of Mechanical Theorem Proving in Geometries, Volume 1: Part of Elementary Geometries, Science Press, Beijing (in Chinese), 1984. English Edition, Springer-Verlag, 1994.Google Scholar
  24. 24.
    L. Yang, Computer-Aided Proving for New Theorems of non-Euclidean Geometry, Research Report, No.4, Mathematics Research Section, Australian National University, 1989.Google Scholar
  25. 25.
    J. Z. Zhang, L. Yang, & M. Deng, The Parallel Numerical Method of Mechanical Theorem Proving, Theoretical Computer Science, 74, 253–271, 1990.CrossRefGoogle Scholar
  26. 26.
    J. Z. Zhang, L. Yang, & X. Hou, A Criterion for Dependency of Algebraic Equations, with Applications to Automated Theorem Proving, Science in China Ser.A, 37, 547–554,1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Lu Yang
    • 1
  • Xiao-Shan Gao
    • 2
  • Shang-Ching Chou
    • 3
  • Jing-Zhong Zhang
    • 1
  1. 1.Chengdu Institute of Computer ApplicationsAcademia SinicaChina
  2. 2.Institute of Systems ScienceAcademia SinicaChina
  3. 3.Department of Computer ScienceThe Wichita State UniversityWichita

Personalised recommendations