Dealing with Degeneracies in Automated Theorem Proving in Geometry

Zoltán Kovács, Tomas Recio, Luis F. Tabera and M. Pilar Vélez
Additional contact information
Zoltán Kovács: The Private University College of Education of the Diocese of Linz, Salesianumweg 3, 4020 Linz, Austria
Tomas Recio: Departamento de Ingeniería Industrial, Escuela Politécnica Superior, Universidad Antonio de Nebrija, C/Pirineos 55, 28040 Madrid, Spain
Luis F. Tabera: Departamento de Matemáticas, Estadística y Computación, Facultad de Ciencias, Universidad de Cantabria, Avenida de los Castros, 39071 Santander, Spain
M. Pilar Vélez: Departamento de Ingeniería Industrial, Escuela Politécnica Superior, Universidad Antonio de Nebrija, C/Pirineos 55, 28040 Madrid, Spain

Mathematics, 2021, vol. 9, issue 16, 1-17

Abstract: We report, through different examples, the current development in GeoGebra, a widespread Dynamic Geometry software, of geometric automated reasoning tools by means of computational algebraic geometry algorithms. Then we introduce and analyze the case of the degeneracy conditions that so often arise in the automated deduction in geometry context, proposing two different ways for dealing with them. One is working with the saturation of the hypotheses ideal with respect to the ring of geometrically independent variables, as a way to globally handle the statement over all non-degenerate components. The second is considering the reformulation of the given hypotheses ideal—considering the independent variables as invertible parameters—and developing and exploiting the specific properties of this zero-dimensional case to analyze individually the truth of the statement over the different non-degenerate components.

Keywords: automated theorem proving in geometry; automated deduction in geometry; automated reasoning in geometry; Dynamic Geometry; GeoGebra; computational algebraic geometry (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2021
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
https://www.mdpi.com/2227-7390/9/16/1964/pdf (application/pdf)
https://www.mdpi.com/2227-7390/9/16/1964/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:9:y:2021:i:16:p:1964-:d:615885

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().