Abstract
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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
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)
Bazzotti, L., Dalzotto, G.: Geometrical theorem-proving, a supported CoCoA package. http://cocoa.dima.unige.it/download/doc/GUI_help/partGeometricalTheoremProving.html
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)
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)
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)
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)
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)
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)
Chou, S.C.: A method for mechanical derivation of formulas in elementary geometry. J. Autom. Reason. 3, 291–299 (1987)
Chou, S.-C.: Mechanical geometry theorem proving. In: Mathematics and its Applications. D. Reidel, Dordrecht (1988)
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)
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 http://cocoa.dima.unige.it
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)
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)
Kapur, D.: Wu’s method and its application to perspective viewing. In: Kapur, D., Mundy, J.L. (eds.) Geometric Reasoning. MIT, Cambridge (1989)
Koepf, W.: Gröbner bases and triangles. Int. J. Comp. Algebra Math. Educ. 4(4), 371–386 (1998)
Kreuzer, M., Robbiano, L.: Computational Commutative Algebra 1. Springer, New York (2000)
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)
Recio, T.: Cálculo Simbólico y Geométrico. Editorial Síntesis. Madrid (1998)
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)
Recio, T., Pilar Vélez, M.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (1999)
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)
Richard, P.: Raisonnement et stratégies de preuve dans l’enseignement des mathématiques. Peter Lang Editorial, Berne (2004)
Wang, D.: A new theorem discovered by computer prover. J. Geom. 36, 173–182 (1989) (preprint 1986)
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)
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)
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)
Wang, D.: Elimination Practice: Software Tools and Applications. Imperial College Press, London (2004)
Author information
Authors and Affiliations
Corresponding author
Additional information
Last author supported by grant “Algoritmos en Geometría Algebraica de Curvas y Superficies” (MTM2008-04699-C03-03) from the Spanish MICINN.
Rights and permissions
About this article
Cite this article
Dalzotto, G., Recio, T. On Protocols for the Automated Discovery of Theorems in Elementary Geometry. J Autom Reasoning 43, 203–236 (2009). https://doi.org/10.1007/s10817-009-9133-x
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-009-9133-x