Skip to main content
Log in

Detecting truth, just on parts

  • Published:
Revista Matemática Complutense Aims and scope Submit manuscript

Abstract

We introduce, through a computational algebraic geometry approach, the automatic reasoning handling of propositions that are simultaneously true over some relevant collections of instances and false over some relevant collections of instances. A rigorous, algorithmic criterion is presented for detecting such cases, and its performance is exemplified through the implementation of this test within the dynamic geometry program GeoGebra. Our framework has some significant differences regarding some alternative, recent formulation of the “true on components” idea; differences and similarities between both approaches are discussed here.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8

Similar content being viewed by others

Notes

  1. But automatically chosen by the program. Roughly: for free points, both coordinates are added in the set. For constrained points (that is, if the point is defined as an arbitrary element of a line or circle or other one-dimensional path), the first coordinate is set to be free, and the second one is considered dependent.

  2. See https://tinyurl.com/hilbertdim for details. The program code is an implementation of the algorithm DIMENSION_2 in [13, p. 19].

References

  1. Botana, F., Hohenwarter, M., Janičić, J., Kovács, Z., Petrović, I., Recio, T., Weitzhofer, S.: Automated theorem proving in GeoGebra: current achievements. J. Autom. Reason. 55, 39–59 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  2. Botana, F., Recio, T.: On the unavoidable uncertainty of truth in dynamic geometry proving. Math. Comput. Sci. 10(1), 5–25 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  3. Chou, S.C.: Mechanical Geometry Theorem Proving. Mathematics and its Applications, vol. 41, D. Reidel Publishing Co., Dordrecht (1988)

  4. Cox, D.A., Little, J., O’Shea, D.: Ideals, varieties, and algorithms. An introduction to computational algebraic geometry and commutative algebra. 4th revised ed. Undergraduate Texts in Mathematics. Springer, Cham (2015)

  5. Dalzotto, G., Recio, T.: On protocols for the automated discovery of theorems in elementary geometry. J. Autom. Reason. 43, 203–236 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Kovács, Z., Recio, T., Vélez, M.P.: GeoGebra automated reasoning tools: a tutorial. https://github.com/kovzol/gg-art-doc/blob/master/pdf/english.pdf (2018). Accessed 23 March 2018

  7. Montes, A., Recio, T.: Automatic discovery of geometry theorems using minimal canonical comprehensive Gröbner systems. In: Botana, F., Recio, T. (eds.) Proceedings Automated Deduction in Geometry 2006. Lecture Notes on Artificial Intelligence, vol. 4869, pp. 13–138. Springer, Berlin (2007)

    Google Scholar 

  8. Ladra,M., Páez-Guillán, M.P., Recio, T.: Two ways of using Rabinowitsch trick for imposing non-degeneracy conditions. In: Narboux, J., Schreck, P., Streinu I. (eds). Proceedings of ADG 2016: Eleventh International Workshop on Automated Deduction in Geometry, pp. 144–152. Strasbourg (2016). http://icubeweb.unistra.fr/adg2016/index.php/Accueil. Accessed 12 July 2018

  9. Losada, R., Recio, T., Valcarce, J.L.: On the automatic discovery of Steiner–Lehmus generalizations (extended abstract). In: Richter-Gebert, J., Schreck, P. (eds.) Proceedings Automated Deduction in Geometry 2010, pp. 171–174. Munich (2010)

  10. Recio, T.: Cálculo Simbólico y Geométrico. Editorial Síntesis, Madrid (1998)

    Google Scholar 

  11. Recio, T., Sterk, H., Vélez, M.P.: Automatic geometry theorem proving. In: Cohen, A.M., Cuipers, H., Sterk, H. (eds.) Some Tapas of Computer Algebra, Algorithms and Computations in Mathematics 4, pp. 276–291. Springer, Berlin (1998)

    Google Scholar 

  12. Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  13. Winkler, F.: Gröbner Bases – Theory and Applications. 5th SCIEnce Training School in Symbolic Computation. RISC, Univ. Linz, 28.6.–9.7.2010. https://www.risc.jku.at/projects/science/school/fifth/materials/GB.pdf (2010). Accessed 23 July 2018

  14. Zariski, O., Samuel, P.: Commutative Algebra, Vol. 2. Graduate Text in Mathematics 29. Springer, Berlin (1960)

  15. Zhou, J., Wang, D., Sun, Y.: Automated reducible geometric theorem proving and discovery by Gröbner basis method. J. Autom. Reason. 59(3), 331–344 (2017)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to M. Pilar Vélez.

Additional information

Partially supported by the Spanish Research Project MTM2017-88796-P.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Kovács, Z., Recio, T. & Vélez, M.P. Detecting truth, just on parts. Rev Mat Complut 32, 451–474 (2019). https://doi.org/10.1007/s13163-018-0286-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s13163-018-0286-1

Keywords

Mathematics Subject Classification

Navigation