Randomized Xero Testing of Radical Expressions and Elementary Geometry Theorem Proving

1. G. Carr’ Ferro and G. Gallo. A procedure to prove geometrical statements. In L. Huguet and A. Poli, editors, Proc. 5th Int. Conf. on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, volume 356 of LNCS, pages 141–150. Springer, Berlin, 1989.

   Google Scholar 

2. G. Carr’ Ferro, G. Gallo, and R. Gennaro. Probabilistic verification of elementary geometry statements. In D. Wang, editor, Proc. Int. Workshop on Automated Deduction in Geometry (ADG-96), volume 1360 of LNAI, pages 87–101. Springer, Berlin, 1997.

   Google Scholar 

3. S.-C. Chou. Proving elementary geometry theorems using Wu’s algorithm. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, volume 29 of Contemporary Mathematics, pages 243–286. American Mathematical Society, Providence, Rhode Island, 1984.

   Google Scholar 

4. S.-C. Chou. Proving geometry theorems using Wu’s method: A collection of geometry theorems proved mechanically. Technical Report 50, Institute for Computing Science, University of Texas, Austin, July 1986.

   Google Scholar 

5. S.-C. Chou. Mechanical Geomtry Theorem Proving. D. Reidel Publishing Company, 1988.

   Google Scholar 

6. P. Conti and C. Traverso. Proving real geometry theorems and the computation of the real radical. In J. Richter-Gebert and D. Wang, editors, Proc. 3rd Int. Workshop on Automated Deduction in Geometry (ADG 2000), pages 109–120. Zurich, Switzerland, Sept. 2000.

   Google Scholar 

7. A. Ferro and G. Gallo. Automatic theorem proving in elementary geometry. Le Matematiche, XLIII(fasc. I):195–224, 1988.

   MathSciNet  Google Scholar 

8. G. Gallo. La Dimostrazione Automatica in Geometria e Questioni di Complessità Correlate. Tesi di dottorato, University of Catania, Italy, 1989.

   Google Scholar 

9. G. Gallo and B. Mishra. Efficient algorithms and bounds forWu-Ritt characteristic sets. In F. Mora and C. Traverso, editors, Effective Methods in Algebraic Geometry (Proc. MEGA’90), volume 94 of Progress in Mathematics, pages 119–142. Birkhäuser, Boston, 1991.

   Google Scholar 

10. G. Gallo and B. Mishra. Wu-Ritt characteristic sets and their complexity. In Computational Geometry: Papers from the DIMACS Special Year, volume 6, pages 111–136. AMS and ACM, New York, 1991.

    Google Scholar 

11. J.-W. Hong. Proving by example and gap theorem. In Proc. 27th Annual Symposium on Foundations of Computer Science, pages 107–116. IEEE, 1986.

    Google Scholar 

12. D. Kapur. Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation, 2:399–412, 1986.

    Article  MATH  MathSciNet  Google Scholar 

13. V. Karamcheti, C. Li, I. Pechtchanski, and C. K. Yap. A core library for robust numeric and geometric computation. In Proc. 15th ACM Symp. on Computational Geometry, pages 351–359. ACM Press, New York, 1999.

    Google Scholar 

14. B. Kutzler and S. Stifter. Automated geometry theorem proving using Buchberger’s algorithm. In Proc. Symp. on Symbolic and Algebraic Computation, pages 209–214. ACM Press, New York, 1986.

    Google Scholar 

15. C. Li. Exact Geometric Computation: Theory and Applications. PhD thesis, Courant Institute of Mathematical Sciences, New York University, Jan. 2001. URL: http://www.cs.nyu.edu/csweb/Research/theses.html.

    Google Scholar 

16. C. Li and C. K. Yap. A new constructive root bound for algebraic expressions. In Proc. 12th ACM-SIAM Symposium on Discrete Algorithms (SODA 2001), pages 496–505. ACM and SIAM, 2001.

    Google Scholar 

17. E. W. Mayr and A. R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46:305–329, 1982.

    Article  MATH  MathSciNet  Google Scholar 

18. K. Mehlhorn and S. Schirra. A generalized and improved constructive separation bound for real algebraic expressions. Technical Report MPI-I-2000-004, Max-Planck-Institut für Informatik, Nov. 2000.

    Google Scholar 

19. K. Ouchi. Real/Expr: Implementation of an exact computation package. Master thesis, Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, Jan. 1997.

    Google Scholar 

20. J. T. Schwartz. Probabilistic verification of polynomial identities. J. ACM, 27(4): 701–717, 1980.

    Article  MATH  Google Scholar 

21. W.-T. Wu. On decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 21:157–179, 1978.

    Google Scholar 

22. W.-T. Wu. Some recent advances in mechanical theorem proving of geometries. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, volume 29 of Contemporary Mathematics, pages 235–242. American Mathematical Society, Providence, Rhode Island, 1984.

    Google Scholar 

23. W.-T. Wu. Basic principles of mechanical theorem proving in elementary geometries. Journal of Automated Reasoning, 2(4):221–252, 1986.

    MATH  Google Scholar 

24. C. K. Yap. A new lower bound construction for commutative Thue systems, with applications. Journal of Symbolic Computation, 12:1–28, 1991.

    Article  MATH  MathSciNet  Google Scholar 

25. C. K. Yap. Robust geometric computation. In J. E. Goodman and J. O’Rourke, editors, Handbook of Discrete and Computational Geometry, chapter 35, pages 653–668. CRC Press LLC, 1997.

    Google Scholar 

26. C. K. Yap. Towards exact geometric computation. Computational Geometry: Theory and Applications, 7:3–23, 1997. Invited talk, Proc. 5th Canadian Conference on Computational Geometry, Waterloo, Aug. 5-9, 1993.

    MATH  MathSciNet  Google Scholar 

27. R. Zippel. Effective Polynomial Computation. Kluwer Academic Publishers, 1993.

    Google Scholar 

Download references