Methods for mechanical geometry formula deriving

ABSTRACT

A precise formulation for the relations among certain variables under a set of polynomial equations and a set of polynomial inequations (to exclude certain special cases which cannot be excluded by the selection of parameters alone) is given. Several methods are presented to find such relations. The methods have been implemented and used to find geometry formulas, to discover geometry theorems, and to find geometry locus equations. About 120 non-trivial problems have been solved using the methods.

REFERENCES

• 1: B. Buchberger, "GrSbner Bases: An Algorithmic Method in Polynomial Ideal Theory", Chapter 6 in Recent Trends in Multidimensional Systems Theory, N.K. Bose (ed.) D. Reidel Publ. Comp. 1985.
• 2: Shang-Ching Chou, A method for the mechanical derivation of formulas in elementary geometry, Journal of Automated Reasoning, v.3 n.3, p.291-299, Sept. 1987
• 3: S.-C. Chou, Mechanical geometry theorem proving, Kluwer Academic Publishers, Norwell, MA, 1987
• 4: Shang Chou , Xiao Gao, Ritt Wu''s Decomposition Algorithm and Geometry Theorem Proving, University of Texas at Austin, Austin, TX, 1990
• 5: Shang Chou , Xiao Gao, Mechanical Formula Derivation in Elementary Geometries, University of Texas at Austin, Austin, TX, 1989
• 6: Shang Chou , Xiao Gao, A Collection of 120 Computer Solved Geometry Problems in Mechanical FormulaDerivation, University of Texas at Austin, Austin, TX, 1989
• 7: S.C. Chou and G.J. Yang, "On the Algebraic Formulation of Certain Geometry Statements and Mechanical Geometry Theorem Proving", Algovithmica, Vol. 4, 1989, 237-262.
• 8: Patrizia Gianni , Barry Trager , Gail Zacharias, Gro¨bner bases and primary decomposition of polynomial ideals, Journal of Symbolic Computation, v.6 n.2-3, p.149-167, Oct./Dec. 1988 [doi>10.1016/S0747-7171(88)80040-3]
• 9: J.F. Rift, Differential Algebra, AMS Colloquium Publications, New York, 1950.
• 10: Wen-Tsun Wu, Basic principles of mechanical theorem proving in elementary geometrics, Journal of Automated Reasoning, v.2 n.3, p.221-252, Aug. 1987 [doi>10.1007/BF02328447]
• 11: Wu Wen-tsiin, "A Mechanization Method of Geometry and its Applications - I: Distances, areas, and volumes", J. of Sys. Set. and Math. Set. Vol 6, 1986, 204-216.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.1 Numerical Algorithms and Problems
          Subjects: Computations on polynomials

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

General Terms:
Algorithms