Examples of automatic theorem proving a real geometry

ABSTRACT

In this paper we show that computer algebra methods in mechanical geometry theorem proving can also be applied to obtain new theorems involving inequalities. An interesting feature is that in real geometry, several cases can occur, none of them being more generic than the other. The examples we give come from the geometry of the triangle, more precisely comparing radii of circles defined in the triangle.

REFERENCES

• AMcC: Dennis S. Arnon , Scott McCallum, A polynomical-time algorithm for the topological type of a real algebraic curve, Journal of Symbolic Computation, v.5 n.1-2, p.213-236, February/April 1988 [doi>10.1016/S0747-7171(88)80013-0]
• BCK: B. Buchberger , G. E. Collins , B. Kutzler, Algebraic methods for geometric reasoning, Annual review of computer science: vol. 3, 1988, Annual Reviews Inc., Palo Alto, CA, 1988
• BCR: : Bochnak J., Coste M., Roy M.F.- G6om~trie alg6briqu r~elle- Ergebnisse der Mathem~tik- Springer Verlag- Berlin - 1987.
• Ch: S.-C. Chou, Mechanical geometry theorem proving, Kluwer Academic Publishers, Norwell, MA, 1987
• Co: George E. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p.134-183, May 20-23, 1975
• Cox: : Coxeter H.S.M.- Introduction to geometry- John Wiley and sons- 1961.
• Gao: : Gao Xiaoshan - Transcendental functions and mechanical theorem proving in elementary geometries- Mathematics Mechanization Research Preprints, Institute of Systems Science, N2- Academia Sinica- 1!}87.
• Gue: Guergueb A. Exemples de d~monsl;ration automatique en g~omdtrie r~dle, Th~se, Universit~ de Kennes I.
• Gr: : Gr6bner W.- Moderne algebraische Geometrie- Springer Verlag- Wien und innsbr6ck- 1949.
• Ho: Hoon Hong, An efficient method for analyzing the topology of plane real algebraic curves, Selected papers presented at the international IMACS symposium on Symbolic computation, new trends and developments, p.571-582, January 1996, Lille, France
• Ma: Mainguen~ J. Feuerback vs Taylor, preprint, Universit~ de Rennes
• Pi: Pinchon D. Oral communication
• Ri: : Ritz J. F. Differential equations from the algebraic standpoint- American :'vlathema~ical Society - New York- 1932.
• Wu1: : Wu Wen-Tsun, On the decisic)n problem and the mechanization of theorem proving in eie:men~ary geometry- Scientia Sinica, 21(1978), re-published in Automated Theorem Proving after 25 years- Bledsoe and Loveland editors- Denver - 1984.
• Wu2: : Wu Wen-Tsun, A mechanization method of geometry and its application Mechanical proving of polynomial inequalities and equations solving- ~athematics Mechanization I~,esearch Preprints, Institute of Systems Science, N2 - Academia Sinica- 1987.
• WG: : Wang Dongming, Gao Xiaoshaal- Geometry theorems proved mechanically using Wus method Mathematics Mechamza~ion Research Preprints, Institute of Systems Science, N2- Academia Sinica- 1987.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Algebraic algorithms

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Geometrical problems and computations
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

General Terms:
Algorithms, Theory, Verification