# Automated geometric reasoning: Dixon resultants, Gröbner bases, and characteristic sets

Conference paper

First Online:

## Abstract

Three different methods for automated geometry theorem proving—a generalized version of Dixon resultants, Gröbner bases and characteristic sets—are reviewed. The main focus is, however, on the use of the generalized Dixon resultant formulation for solving geometric problems and determining geometric quantities.

## Keywords

Theorem Prove Subsidiary Condition Extraneous Factor Elimination Problem Geometry Theorem
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.

## Preview

Unable to display preview. Download preview PDF.

## References

- 1.Arnon, D.S., Collins, G.E., and McCallum, S., Cylindrical algebraic decomposition I: The basic algorithm; II: An adjacency algorithm for the plane.
*SIAM J. of Computing*13, 1984, 865–877, 878–889.CrossRefGoogle Scholar - 2.Becker T., Weispfenning V., in cooperation with Kredel H.,
*Gröbner Bases, A Computational Approach to Commutative Algebra*. Springer-Verlag, New York, 1993.Google Scholar - 3.Buchberger B., Gröbner bases: An algorithmic method in polynomial ideal theory.
*Multidimensional Systems Theory*(ed. Bose), D. Reidel Publ. Co., 1985, 184–232.Google Scholar - 4.Chou, S.-C.,
*Proving and Discovering Theorems in Elementary Geometry using Wu's Method*. Ph.D. Thesis, Dept. of Mathematics, University of Texas, Austin, 1985.Google Scholar - 5.Chou, S.-C.,
*Mechanical Geometry Theorem Proving*. D. Reidel Publishing Company, Dordrecht, Netherlands, 1988.Google Scholar - 6.Chou, S.-C., and Gao, X.-S., Ritt-Wu's decomposition algorithm and geometry theorem proving. Proc.
*10th Intl. Conf. on Automated Deduction (CADE-10)*, Kaiserslautern, LNCS 449, July 1990, 207–220.Google Scholar - 7.Chou, S.-C., and Gao, X.-S., Mechanical formula derivation of elementary geometries. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Tokyo, 1990, 265–270.Google Scholar - 8.Chou, S.-C., and Gao, X.-S., Proving constructive geometry statements. Proc.
*11th Intl. Conf. on Automated Deduction (LADE-11)*, Saratoga Springs, Springer LNAI 607, 1992, 20–34.Google Scholar - 9.Chou, S.-C., Gao, X.-S., and Zhang, J. Z., Automated geometry theorem proving by vector calculations. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Kiev, 1993, 284–291.Google Scholar - 10.Chou, S.-C., Gao, X.-S., and Zhang, J.-Z., Automated production of traditional proofs for constructive geometry theorems. Proc.
*8th Annual IEEE Symp. on Logic in Computer Science (LICS)*, Montreal, June 1994, 48–56.Google Scholar - 11.Chou, S.-C., Gao, X.-S., and Zhang, J.-Z.,
*Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems*. World Scientific Press, 1994.Google Scholar - 12.Chou, S.-C., Gao, X.-S., and Zhang, J. Z., A deductive database approach to automated geometry theorem proving and discovering. Accepted for publication in
*J. of Automated Reasoning*.Google Scholar - 13.Chou, S.-C., and Schelter, W.F., Proving geometry theorems with rewrite rules.
*J. of Automated Reasoning*2 (3), 1986, 253–273.Google Scholar - 14.Coelho, H., and Pereira, L.M., Automated reasoning in geometry theorem proving with PROLOG.
*J. of Automated Reasoning*2 (4), 1986, 329–390.CrossRefGoogle Scholar - 15.Connolly, C.I., Kapur, D., Mundy, J.L., and Weiss, R., GEometer: A System for modeling and algebraic manipulation,
*Proc. DARPA Workshop on Image Understanding*, Palo Alto, May 1989, 797–804.Google Scholar - 16.Conti, P., and Traverso, C., A case of automatic theorem proving in Euclidean geometry: The Maclane 8
_{3}theorem. Proc.*AAECC*, LNCS 948, Paris, 1995, 183–193.Google Scholar - 17.Crapo, H., Automatic proofs of geometry theorems: The synthetic approach, Presented at the
*Intl. Workshop on Automated Deduction in Geometry*, Toulouse, Sept 1996.Google Scholar - 18.Cyrluk, D.A., Harris, R.M., and Kapur, D., GEometer: A theorem prover for algebraic geometry. Proc.
*9th Intl. Conf. on Automated Deduction (LADE-9)*, Argonne, IL, LNCS 310, May 1988. 770–771.Google Scholar - 19.Dixon, A. L., The eliminant of three quantics in two independent variables. Proc.
*London Mathematical Society*6, 1908, 468–478.Google Scholar - 20.Dolzmann, A., Sturm, T., and Weispfenning, V., A new approach for automatic theorem proving in real geometry. Accepted for publication in
*J. of Automated Reasoning*.Google Scholar - 21.Emiris I.,
*Sparse Elimination and Applications in Kinematics*. Ph.D. Thesis, Computer Science Division, University of Calif., Berkeley, 1994.Google Scholar - 22.Gao, X.-S., and Wang, D.-K., On the automatic derivation of a set of geometric formulae.
*J. of Geometry*, 53, 1995, 79–88.CrossRefGoogle Scholar - 23.Gerber, L., The orthocentric simplex as an extreme simplex.
*Pacific J. of Mathematics*56, 1975, 97–111.Google Scholar - 24.Herstein, I. N.,
*Topics in Algebra*-*Second Edition*. John Wiley & Sons, Inc., USA, 1975.Google Scholar - 25.Heymann, W. Problem der Winkehalbierenden.
*Ztschr. f. Math. and Phys.*35, 1890.Google Scholar - 26.Hong, J., Proving by example and the gap theorems. Proc
*27th Annual Symp. on Foundations of Computer Science (FOCS)*, Toronto, Oct. 1986, 107–116.Google Scholar - 27.Huang, Y.Z., and Wu, W.D., Kinematic solution of a Stewart platform. Proc.
*1992 Intl. Workshop on Mathematics Mechanization*(eds. Wu and Cheng), Intl. Academic Publishers, 1992, 181–188.Google Scholar - 28.Kapur, D., Geometry theorem proving using Hilbert's Nullstellensatz. Proc.
*1986 Symposium on Symbolic and Algebraic Computation (SYMSAC 86)*, Waterloo, 1986, 202–208.Google Scholar - 29.Kapur, D., A refutational approach to geometry theorem proving.
*Artificial Intelligence*, 37, 1988, 61–94.CrossRefGoogle Scholar - 30.Kapur, D., Algorithmic elimination methods. Tutorial Notes,
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Montreal, July 1995.Google Scholar - 31.Kapur, D., and Lakshman, Y., Elimination methods: An introduction.
*Symbolic and Numerical Computation for Artificial Intelligence*(eds. Donald, Kapur and Mundy), Academic Press, 1992, 45–87.Google Scholar - 32.Kapur, D., Y.N., Lakshman, and Saxena, T., Computing invariants using elimination methods. Proc.
*IEEE Intl. Symp. on Computer Vision*, Coral Gables, Florida, November 1995.Google Scholar - 33.Kapur, D., and Mundy, J.L., Wu's method and its application to perspective viewing.
*Artificial Intelligence*, 37, 1988, 15–26.CrossRefGoogle Scholar - 34.Kapur, D., and Saxena, T., Automated geometry theorem proving'using the Dixon resultants. Invited Talk,
*IMACS-95*, Albuquerque, New Mexico, May 1995.Google Scholar - 35.Kapur, D., and Saxena, T., Comparison of various multivariate resultant formulations. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Montreal, July 1995, 187–194.Google Scholar - 36.Kapur, D., and Saxena, T., Sparsity considerations in the Dixon resultant formulation, Proc.
*ACM Symposium on Theory of Computing (STOC)*, Philadelphia, May 1996, 184–191Google Scholar - 37.Kapur, D., and Saxena, T., Extraneous factors in the Dixon resultant formulations. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Hawaii, July 1997, 141–148.Google Scholar - 38.Kapur D., Saxena T. and Yang L., Algebraic and geometric reasoning using Dixon resultants. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Oxford, July 1994, 99–107.Google Scholar - 39.Kapur, D., and Wan, H., Refutational proofs of geometry theorems via characteristic set computation. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Tokyo, August 1990, 277–284.Google Scholar - 40.Knuth, D.E.,
*Seminumerical Algorithms: The Art of Computer Programming*. Vol. 2, Second Edition, Addison Wesley, 1980, 407–408.Google Scholar - 41.Ko, H.P., and Hussain, M.A., A study of Wu's method—A method to prove certain theorems in elementary geometry. Proc.
*1985 Congressus Numerantium*, 1985Google Scholar - 42.Kutzler, B., and Stifter, S., Automated geometry theorem proving using Buchberger's algorithm. Proc.
*1986 Symposium on Symbolic and Algebraic Computation (SYMSAC 86)*, Waterloo, 1986, 209–214.Google Scholar - 43.Lazard D., Generalized Stewart platform: How to compute with rigid motions?
*Proc. IMACS-SC*, Lille, June 1993, 85–88.Google Scholar - 44.Li, H., and Cheng, M., Proving theorems in elementary geometry with Clifford algebraic method. Preprint, MMRC, Academia Sinica, China, 1995.Google Scholar
- 45.Mourrain B., The 40 “generic” positions of a parallel robot.
*Proc. ACM Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Kiev, July 1993.Google Scholar - 46.Mundy, J., L., Zisserman, A., Towards a new framework for vision.
*Geometric Invariance in Computer Vision*(eds. Mundy and Zisserman), MIT Press, 1992, 1–39.Google Scholar - 47.Recio, T., and Velez-Melon, M.P., Automatic discovery of theorems in elementary geometry. Presented at the
*Workshop on Automated Deduction in Geometry*, Toulouse, Sept 1996.Google Scholar - 48.Rege, A., A complete and practical algorithm for geometric theorem proving. Proc
*11th Annual Symp. on Computational Geometry*, Vancouver, June 1995, 277–286.Google Scholar - 49.Richter-Gebert, J., Mechanical theorem proving in projective geometry.
*Algebraic Approaches to Geometric Reasoning*(eds. Hong, Wang, and Winkler), A special issue of Annals of Mathematics and Artificial Intelligence, 1995.Google Scholar - 50.Ritt, J.F.,
*Differential Algebra*. AMS Colloquium Publications, 1950.Google Scholar - 51.Ronga F., and Vust T., Stewart platforms without computer.
*Preprint*, Department of Mathematics, University of Geneva, 1992.Google Scholar - 52.Saxena, T.,
*Efficient Variable Elimination using Resultants*. Ph.D. Thesis, Dept. of Computer Science, State University of New York, Albany, Nov. 1996.Google Scholar - 53.Stifter, S., Geometry theorem proving in vector spaces by means of Gröbner bases. Proc.
*Intl. Symp. on Symbolic and Algebraic Computation (ISSAC)*, Kiev, July 1993, 301–310.Google Scholar - 54.Sykes, M.,
*A Source Book of Problems for Geometry, based upon Industrial Design and Architectural Ornament*. Boston, Allyn and Bacon, 1912.Google Scholar - 55.Tarski, A., A Decision Method for Elementary Algebra and Geometry. U. of Calif. Press, 1948; 2nd edition, 1951.Google Scholar
- 56.Wan, H.,
*Refutational Proofs of Geometry Theorems using the Characteristic Set Method*. MS project, RPI, Troy, NY, 1987.Google Scholar - 57.Wang, D., Proving-by-examples method and inclusion of varieties.
*Kexue Tongbao*, 33, 1988, 1121–1123.MathSciNetGoogle Scholar - 58.Wang, D., A new theorem discovered by computer prover.
*J. of Geometry*, 36, 1989, 173–182.CrossRefGoogle Scholar - 59.Wang, D., Algebraic factoring and geometry theorem proving. Proc.
*12th Intl. Conf. on Automated Deduction (CADE-12)*, Nancy, LNAI 814, 1994, 386–400.Google Scholar - 60.Wang, D., Geometry machines: From AI to SMC. Proc.
*Intl. Conf. on Artificial Intelligence and Symbolic Mathematical Computation (AISMC-3)*, Steyr, Austria, 1996, LNCS 1138, 213–239.Google Scholar - 61.Wang, D., and Gao, X.-S., Geometry theorems proved mechanically using Wu's method—Part on Euclidean geometry.
*MM Research Preprints*, 2, 1987, 75–106.Google Scholar - 62.Wit, W., On the decision problem and the mechanization of theorem proving in elementary geometry.
*Scientia Sinica*21 (1978) 150–172. Also in*Automated Theorem Proving: After 25 Years, Contemporary Mathematics*29 (eds. Bledsoe and Loveland), 1984, 213–234.Google Scholar - 63.Wu, W., Some recent advances in mechanical theorem proving of geometries.
*Automated Theorem Proving: After 25 Years, Contemporary Mathematics*29 (eds. Bledsoe and Loveland), 1984, 235–241.Google Scholar - 64.Wu, W., Basic principles of mechanical theorem proving in geometries.
*J. of System Sciences and Mathematical Sciences*4 (3), 1984, 207–235. Also in*J. of Automated Reasoning*2, 1986, 221–252.Google Scholar - 65.Wu, W., A mechanization method of geometry and its applications.
*J. of System Sciences and Mathematical Sciences*6 (3), 1986, 204–216.Google Scholar - 66.Wu, W., On reducibility problem in mechanical theorem proving of elementary geometries.
*Chinese Quart. J. Mathematics*, 2, 1987, 1–20.Google Scholar - 67.Wu, W., On zeros of algebraic equations—An application of Ritt's principle.
*Kexue Tongbao*, 31 (1), 1986, 1–5.Google Scholar - 68.Wu, W.,
*Mechanical Theorem Proving in Geometries: Basic Principles*. Translated from Chinese by Jin and Wang, Springer Verlag, 1994.Google Scholar - 69.Yang, L., Zhang, J.-Z., and Hou, X.-R., An efficient decomposition algorithm for geometry theorem proving without factorization. Proc.
*ASCM'95*, Beijing, August 1995, 33–41.Google Scholar - 70.Yang, L., Zhang, J.-Z., and Li, C.-Z., A prover for parallel numerical verification of a class of constructive geometry theorems. Proc.
*Intl. Workshop on Mechanization of Mathematics*(ed. Wu and Cheng), Beijing, China, July 1992, 244–250.Google Scholar - 71.Zhang, J. Z., Chou, S.-C., and Gao, X.-S., Automated production of traditional proofs for theorems in Euclidean geometry I.
*Algebraic Approaches to Geometric Reasoning*(eds. Hong, Wang, and Winkler), A special issue of Annals of Mathematics and Artificial Intelligence, 1995, 109–137.Google Scholar - 72.Zhang, J.-Z., Yang, L., and Deng, M.-K., The parallel numerical method of mechanical theorem proving.
*Theoretical Computer Science*, 74, 1990, 253–271.CrossRefGoogle Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1998