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

## Abstract

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.

## Keywords

Theorem Prove Elliptic Geometry Hyperbolic Geometry Geometric Quantity Automate Theorem Prove## Preview

Unable to display preview. Download preview PDF.

## References

- 1.S. C. Chou,
*Mechanical Geometry Theorem Proving*, D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.Google Scholar - 2.S. C. Chou, X. S. Gao, & J. Z. Zhang,
*Machine Proofs in Geometry*, World Scientific Pub., Singapore, 1994.Google Scholar - 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.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.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.H. Coelho & L. M. Pereira, Automated Reasoning in Geometry with Prolog,
*J. of Automated Reasoning*, 2, 329–390, 1987.CrossRefGoogle Scholar - 7.H. S. M. Coxeter,
*Non-Euclidean Geometry*, Univ. of Toronto Press, 1968.Google Scholar - 8.X. S. Gao, Transcendental Functions and Mechanical Theorem Proving in Elementary Geometries,
*J. of Automated Reasoning*, 6, 403–417, 1990.Google Scholar - 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.M. J. Greenberg,
*Euclidean Geometry and non-Euclidean Geometry, Development and History*, Freeman, 1980.Google Scholar - 11.B. Grünbaum & G. C. Shephard, From Mennelaus to Computer Assisted Proofs in Geometry, Preprint, Washington State University, 1993.Google Scholar
- 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.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.A. J. Nevins, Plane Geometry Theorem Proving Using Forward Chaining,
*Artificial Intelligence*, 6, 1–23, 1976.CrossRefGoogle Scholar - 15.D. Kapur, Geometry Theorem Proving Using Hilbert's Nullstellensatz,
*Proc. of SYMSAC'86*, Waterloo, pp. 202–208, 1986.Google Scholar - 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.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.T. E. Stokes,
*On the Algebraic and Algorithmic Properties of Some Generalized Algebras*, Ph.D thesis, University of Tasmania, 1990.Google Scholar - 19.A. Tarski,
*A Decision Method for Elementary Algebra and Geometry*, Univ. of California Press, Berkeley, 1951.Google Scholar - 20.D. M. Wang, On Wu's Method for Proving Constructive Geometry Theorems,
*Proc. IJCAI'89*, Detroit, pp. 419–424, 1989.Google Scholar - 21.D. M. Wang, Elimination Procedures for Mechanical Theorem Proving in Geometry,
*Ann. of Math. and AI*, 13, 1–24, 1995.Google Scholar - 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.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.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.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.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