Probabilistic verification of elementary geometry statements

  • Giuseppa Carrá Ferro
  • Giovanni Gallo
  • Rosario Gennaro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1360)


In this paper a probabilistic approach to automated theorem proving in elementary geometry is shown. Bounds on the effective Hilbert Nullstellensatz and on the degree of a Ritt characteristic set are used together with Schwartz's probabilistic results on polynomial identities.


Theorem Prove Elementary Geometry Polynomial Identity Differential Algebra Automate Theorem Prove 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    D. Brownawell: Bounds for the Degree in the Nullstellensatz. Ann. Math. 126 (1987),577–591Google Scholar
  2. 2.
    L. Caniglia, A. Galligo, J. Heintz: Borne simple exponentielle pour le degrés dans le théorème des zéros sur un corps de caractéristique quelconque. C.R.A.S. Paris 307 (1988), 255–258Google Scholar
  3. 3.
    G. Carri, G. Gallo: A Procedure to Prove Geometrical Statements. Proc. AAECC5 (Menorca) Lecture Notes in Computer Science 365 (1986), 141–150Google Scholar
  4. 4.
    S.-C. Chou: Mechanical Geometry Theorem Proving. D. Reidel Publishing Company, Kluwer Academic Publishers Group, Dordrecht Boston (1988)Google Scholar
  5. 5.
    S.-C. Chou: Proving and Discovering Theorems in Elementary Geometries Using Wu's Method. PhD. Thesis, Department of Mathematics, University of Texas at Austin (1985)Google Scholar
  6. 6.
    M.K. Deng: The Parallel Numerical Method of Proving the Constructive Geometric Theorems. Chinese Sci. Bull. 34 (1989), 1066–1070Google Scholar
  7. 7.
    N. Fitchas, A. Galligo: Nulstellensatz effective et conjecture de Serre (Theoreme de Quillen-Suslin) pour le calcul formel. Math. Nachr. 149 (1990), 231–253Google Scholar
  8. 8.
    G. Gallo: La Dimostrazione Automatica in Geometria e Questioni di Complessita' Correlate. Tesi di Dottorato di Ricerca, Catania (1989)Google Scholar
  9. 9.
    G. Gallo, B. Mishra: Efficient Algorithms and Bounds for Wu-Ritt Characteristic Sets. Progress in Math. 94, Proc. of MEGA 90, Birkhäuser (1990), 119–142Google Scholar
  10. 10.
    G. Gallo, B. Mishra: Wu-Ritt Characteristic Sets and Their Complexity. DIMACS series in Discrete Mathematics and Theoretical Computer Science 6 (1991), 111–136Google Scholar
  11. 11.
    J.W. Hong: Proving by Example and Gap Theorem. 27th Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press (1986), 107–116Google Scholar
  12. 12.
    D. Kapur: Using Gröbner Bases to Reason about Geometry Problems. Journal of Symbolic Computation 2 (1986), 399–408MathSciNetGoogle Scholar
  13. 13.
    D. Kapur, T. Saxena, L. Yang: Algebraic and Geometric Reasoning using Dixon Resultants. Proc. ISSAC-94 (Oxford, July 20–22, 1994), 97–107Google Scholar
  14. 14.
    J. Kollar: Sharp Effective Nullstellensatz. J. Amer. Math. Soc. 1 (1988), 963–975Google Scholar
  15. 15.
    B. Kutzler, S. Stifter: Automated Geometry Theorem Proving Using Buchberger's Algorithm. Proceedings of the 1986 Symposium on Symbolic and Algebraic Computation (Waterloo, July 21–23, 1986), 209–214Google Scholar
  16. 16.
    B. Mishra: Algorithmic Algebra. Springer Verlag, New York (1993)Google Scholar
  17. 17.
    J.F. Ritt: Differential Equations from an Algebraic Standpoint. AMS Colloquium Publications XIV, New York (1932)Google Scholar
  18. 18.
    J.F. Ritt: Differential Algebra. AMS Colloquium Publications XXXII, New York (1950)Google Scholar
  19. 19.
    J.T. Schwartz: Fast Probabilistic Algorithms for Verification of Polynomial Identities. Journal of ACM 27 (1980), 701–717CrossRefGoogle Scholar
  20. 20.
    D. Wang: Proving-by-Examples Method and Inclusion of Varieties. Kexue Tongbao 33(4) (1988), 2015–2018Google Scholar
  21. 21.
    D. Wang: Elimination Procedures for Mechanical Theorem Proving in Geometry. Ann. Math. Artif. Intell. 3 (1995), 1–24CrossRefGoogle Scholar
  22. 22.
    D. Wang: Geometry Machines: From AI to SMC. Proc. AISMC-3 (Steyr, Sept. 23-25) Lecture Notes in Computer Science 1138 (1996), 213–239Google Scholar
  23. 23.
    F. Winkler: A Geometric Decision Algorithm Based on the Gröbner Bases Algorithm. Proc. ISSAC-88 (Rome) Lecture Notes in Computer Science 358 (1988), 356–363Google Scholar
  24. 24.
    W-T. Wu: On the Decision Problem and the Mechanization of Theorem Proving in Elementary Geometry. Scientia Sinica 21 (1978), 157–179Google Scholar
  25. 25.
    W-T. Wu: Basic Principles of Mechanical Theorem Proving in Elementary Geometries. Journal of Sys. Sci. and Math. Sci. 4 (1984), 207–235; also in Journal of Automated Reasoning 4 (1986), 221–252Google Scholar
  26. 26.
    26.W-T. Wu: Some Recent Advances in Mechanical Theorem-Proving of Geometries. Automated Theorem Proving: After 25 Years, Contemporary Mathematics. American Mathematical Society. 29 (1984), 235–242Google Scholar
  27. 27.
    W-T. Wu: Mechanical Theorem Proving in Geometries: Basic Principles (translated from the Chinese by Xiaofan Jin and Dongming Wang). Springer-Verlag, Wien New York (1994)Google Scholar
  28. 28.
    L. Yang:A New Method of Automated Theorem Proving. The Mathematical Revolution Inspired by Computing. Oxford Univ. Press, New York (1991), 115–126Google Scholar
  29. 29.
    L. Yang, J.Z. Zhang, C.Z. Li: A Prover for Parallel Numerical Verification of a Class of Constructive Geometry Theorems. Proc. IWMM 92 (Beijing, July 16–18, 1992),244–250Google Scholar
  30. 30.
    L. Yang, J.Z. Zhang: Searching Dependency between Algebraic Equations: An Algorithm Applied to Automated Reasoning. Artificial Intelligence in Mathematics, Oxford University Press, Oxford (1994), 147–156Google Scholar
  31. 31.
    J.Z. Zhang, L. Yang, M.K. Deng: The Parallel Numerical Methods in Mechanical Theorem Proving. Theoret. Comput. Sci. 74 (1990), 253–271CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Giuseppa Carrá Ferro
    • 1
  • Giovanni Gallo
    • 1
  • Rosario Gennaro
    • 2
  1. 1.Dep. of MathematicsUniversity of CataniaCataniaItaly
  2. 2.IBM T.J. Watson Research CenterYorktown HeightsUSA

Personalised recommendations