Dealing with degeneracies in automated theorem proving in geometryA zero-dimensional approach

  1. Zoltán Kovács 1
  2. Tomas Recio 2
  3. Tabera, Luis F. 3
  4. M. Pilar Vélez 2
  1. 1 Private University College of Education of the Diocese of Linz
    info

    Private University College of Education of the Diocese of Linz

    Linz, Austria

    ROR https://ror.org/00wb8n271

  2. 2 Universidad Nebrija
    info

    Universidad Nebrija

    Madrid, España

    ROR https://ror.org/03tzyrt94

  3. 3 Universidad de Cantabria
    info

    Universidad de Cantabria

    Santander, España

    ROR https://ror.org/046ffzj20

Show affiliations +
Book:
EACA 2022: XVII Encuentro de Álgebra Computacional y Aplicaciones
  1. Galindo Pastor, Carlos (coord.)
  2. Gimenez, Philippe (coord.)
  3. Hernando Carrillo, Fernando (coord.)
  4. Monserrat Delpalillo, Francisco José (coord.)
  5. Moyano-Fernández, Julio José (coord.)

Publisher: Servei de Comunicació i Publicacions ; Universitat Jaume I

ISBN: 978-84-19647-46-7

Year of publication: 2023

Pages: 111-114

Congress: Encuentro de Álgebra Computacional y Aplicaciones (17. 2022. Castelló de la Plana)

Type: Conference paper

DIALNET GOOGLE SCHOLAR lock_openRepositori UJI editor

Abstract

In the presentation we will start by reporting, using various examples to present the current development in GeoGebra of geometric automated reasoning tools by means of computational algebraic geometry algorithms. "Ve will then introduce andanalyze 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. The first is to work with the saturation of the hypotheses ideal with respect to the ring ofgeometrically independent variables, as a way to globally handle the statement over all non-degenerate components. The second is to consider the reformulation of the given hypotheses ideal considering the independent variables as invertible parameters, exploiting the specific properties of this zero-dimensional case to analyze the truth of the statement over each non-degenerate component.

Data source: Dialnet