Journal of Automated Reasoning

, Volume 43, Issue 2, pp 203–236 | Cite as

On Protocols for the Automated Discovery of Theorems in Elementary Geometry



In this paper we consider the problem of dealing automatically with arbitrary geometric statements (including, in particular, those that are generally false) aiming to find complementary hypotheses for the statements to become true. Our approach proceeds within the framework of computational algebraic geometry. First we argue and propose a plausible protocol for automatic discovery, and then we present some algorithmic criteria, as well as the meaning (regarding the algebraic geometry of the varieties involved in the given statement), for the protocol success/failure. A detailed collection of examples in also included.


Automatic theorem proving Automatic theorem discovery Elementary geometry Computational algebraic geometry 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bazzotti, L., Dalzotto, G., Robbiano, L.: Remarks on geometric theorem proving. In: Automated Deduction in Geometry, Zurich, 2000. Lecture Notes in Comput. Sci. vol. 2061, pp. 104–128. Springer, Berlin (2001)CrossRefGoogle Scholar
  2. 2.
    Bazzotti, L., Dalzotto, G.: Geometrical theorem-proving, a supported CoCoA package.
  3. 3.
    Beltrán, C., Dalzotto G., Recio, T.: The moment of truth in automatic theorem proving in elementary geometry. In: Botana, F., Roanes-Lozano, E. (eds.) Proceedings ADG 2006 (Extended Abstracts), Universidad de Vigo (2006)Google Scholar
  4. 4.
    Botana, F., Recio, T.: Towards solving the dynamic geometry bottleneck via a symbolic approach. In: Proceedings ADG (Automatic Deduction in Geometry) 2004. Lec. Not. Artificial Intelligence LNAI vol. 3763, pp. 761–771. Springer, New York (2005)Google Scholar
  5. 5.
    Botana, F.: Bringing more intelligence to dynamic geometry by using symbolic computation. In: Li, S., Wang, D., Zhang, J.-Z. (eds.) Symbolic Computation and Education, pp. 136–150. World Scientific, Singapore (2007)Google Scholar
  6. 6.
    Bulmer, M., Fearnley-Sander, D., Stokes, T.: The kinds of truth of geometric theorems. In: Automated Deduction in Geometry, Zurich, 2000. Lecture Notes in Comput. Sci., vol. 2061, pp. 129–142. Springer, Berlin (2001)CrossRefGoogle Scholar
  7. 7.
    Chen, X.F., Li, P., Lin, L., Wang, D.K.: Proving geometric theorems by partitioned-parametric Groebner bases. In: Automated Deduction in Geometry. LNAI, vol. 3763, pp. 34–43. Springer, New York (2006)CrossRefGoogle Scholar
  8. 8.
    Chou, S.-C.: Proving elementary geometry theorems using Wu’s algorithm. In: Contemporary Mathematics, vol. 29, pp. 243–286. Automated Theorem Proving: After 25 Years. American Mathematical Society, Providence (1984)Google Scholar
  9. 9.
    Chou, S.C.: A method for mechanical derivation of formulas in elementary geometry. J. Autom. Reason. 3, 291–299 (1987)MATHCrossRefGoogle Scholar
  10. 10.
    Chou, S.-C.: Mechanical geometry theorem proving. In: Mathematics and its Applications. D. Reidel, Dordrecht (1988)Google Scholar
  11. 11.
    Chou, S.-C., Gao, X.-S.: Methods for mechanical geometry formula deriving. In: Proceedings of International Symposium on Symbolic and Algebraic Computation, pp. 265–270. ACM, New York (1990)CrossRefGoogle Scholar
  12. 12.
    Capani, A., Niesi, G., Robbiano, L.: CoCoA, a system for doing computations in commutative algebra. The version 4.6 is available at the web site
  13. 13.
    Conti, P., Traverso, C.: A case of automatic theorem proving in Euclidean geometry: the Maclane 83 theorem. In: Applied Algebra, Algebraic Algorithms and Error-Correcting Codes (Paris, 1995). Lecture Notes in Comput. Sci., vol. 948, pp. 183–193. Springer, Berlin (1995)Google Scholar
  14. 14.
    Conti, P., Traverso, C.: Algebraic and semialgebraic proofs: methods and paradoxes. In: Automated Deduction in Geometry (Zurich, 2000). Lecture Notes in Comput. Sci., vol. 2061, pp. 83–103. Springer, Berlin (2001)CrossRefGoogle Scholar
  15. 15.
    Kapur, D.: Wu’s method and its application to perspective viewing. In: Kapur, D., Mundy, J.L. (eds.) Geometric Reasoning. MIT, Cambridge (1989)Google Scholar
  16. 16.
    Koepf, W.: Gröbner bases and triangles. Int. J. Comp. Algebra Math. Educ. 4(4), 371–386 (1998)Google Scholar
  17. 17.
    Kreuzer, M., Robbiano, L.: Computational Commutative Algebra 1. Springer, New York (2000)Google Scholar
  18. 18.
    Montes, A., Recio, T.: Automatic discovery of geometry theorems using minimal canonical comprehensive Groebner systems. In: Botana, F., Recio, T. (eds.) Automated Deduction in Geometry. LNAI (Lect. Notes Artificial Intelligence), vol. 4869, pp. 113–139. Springer, New York (2007)CrossRefGoogle Scholar
  19. 19.
    Recio, T.: Cálculo Simbólico y Geométrico. Editorial Síntesis. Madrid (1998)Google Scholar
  20. 20.
    Recio, T., Sterk, H., Pilar Vélez, M.: Automatic geometry theorem proving. In: Cohen, A., Cuypers, H., Sterk, H. (eds.) Some Tapas of Computer Algebra (Algorithms and Computation in Mathematics, vol. 4). Springer, New York (1999)Google Scholar
  21. 21.
    Recio, T., Pilar Vélez, M.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (1999)MATHCrossRefGoogle Scholar
  22. 22.
    Recio, T., Botana, F.: Where the truth lies (in automatic theorem proving in elementary geometry). In: Proceedings ICCSA (International Conference on Computational Science and its Applications) 2004. Lec. Not. Com. Sci., vol. 3044, pp. 761–771. Springer, New York (2004)Google Scholar
  23. 23.
    Richard, P.: Raisonnement et stratégies de preuve dans l’enseignement des mathématiques. Peter Lang Editorial, Berne (2004)Google Scholar
  24. 24.
    Wang, D.: A new theorem discovered by computer prover. J. Geom. 36, 173–182 (1989) (preprint 1986)MATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Wang, D.: On Wu’s method for proving constructive geometric theorems. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence (IJCAI-89), Detroit, USA, 20–25 August 1989, pp. 419–424. Morgan Kaufmann, Los Altos (1989)Google Scholar
  26. 26.
    Wang, D.: Gröbner bases applied to geometric theorem proving and discovering. In: Buchberger, B., Winkler, F. (eds.) Gröbner Bases and Applications, London Mathematical Society Lecture Notes Series, vol. 251, pp. 281–301. Cambridge University Press, Cambridge (1998)Google Scholar
  27. 27.
    Wang, D., Zhi, L.: Algebraic factorization applied to geometric problems, In: Proceedings of the Third Asian Symposium on Computer Mathematics (ASCM ’98), pp. 23–36. Lanzhou University Press, Lanzhou (1998)Google Scholar
  28. 28.
    Wang, D.: Elimination Practice: Software Tools and Applications. Imperial College Press, London (2004)MATHGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2009

Authors and Affiliations

  1. 1.University of PisaPisaItaly
  2. 2.Universidad de CantabriaSantanderSpain

Personalised recommendations