Reseña: A decision procedure for univariate real polynomials in Isabelle/HOL
Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre álgebra titulado A decision procedure for univariate real polynomials in Isabelle/HOL.
Su autor es Manuel Eberl (de la Technische Universität München, Alemania).
Su resumen es
Sturm sequences are a method for computing the number of real roots of a univariate real polynomial inside a given interval efficiently. In this paper, this fact and a number of methods to construct Sturm sequences efficiently have been formalised with the interactive theorem prover Isabelle/HOL. Building upon this, an Isabelle/HOL proof method was then implemented to prove interesting statements about the number of real roots of a univariate real polynomial and related properties such as non-negativity and monotonicity.
El trabajo se ha presentado en la CPP 2015 (The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.