IDEAS home Printed from https://ideas.repec.org/a/gam/jmathe/v9y2021i16p1964-d615885.html
   My bibliography  Save this article

Dealing with Degeneracies in Automated Theorem Proving in Geometry

Author

Listed:
  • Zoltán Kovács

    (The Private University College of Education of the Diocese of Linz, Salesianumweg 3, 4020 Linz, Austria
    These authors contributed equally to this work.)

  • Tomas Recio

    (Departamento de Ingeniería Industrial, Escuela Politécnica Superior, Universidad Antonio de Nebrija, C/Pirineos 55, 28040 Madrid, Spain
    These authors contributed equally to this work.)

  • 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
    These authors contributed equally to this work.)

  • M. Pilar Vélez

    (Departamento de Ingeniería Industrial, Escuela Politécnica Superior, Universidad Antonio de Nebrija, C/Pirineos 55, 28040 Madrid, Spain
    These authors contributed equally to this work.)

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.

Suggested Citation

  • Zoltán Kovács & Tomas Recio & Luis F. Tabera & M. Pilar Vélez, 2021. "Dealing with Degeneracies in Automated Theorem Proving in Geometry," Mathematics, MDPI, vol. 9(16), pages 1-17, August.
    • Handle: RePEc:gam:jmathe:v:9:y:2021:i:16:p:1964-:d:615885
    as

    Download full text from publisher

    File URL: https://www.mdpi.com/2227-7390/9/16/1964/pdf
    Download Restriction: no
    File URL: https://www.mdpi.com/2227-7390/9/16/1964/
    Download Restriction: no
    ---><---

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. José Ramón Trillo & Francisco Javier Cabrerizo & Francisco Chiclana & María Ángeles Martínez & Francisco Mata & Enrique Herrera-Viedma, 2022. "Theorem Verification of the Quantifier-Guided Dominance Degree with the Mean Operator for Additive Preference Relations," Mathematics, MDPI, vol. 10(12), pages 1-10, June.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:gam:jmathe:v:9:y:2021:i:16:p:1964-:d:615885. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: MDPI Indexing Manager (email available below). General contact details of provider: https://www.mdpi.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.