Menu Close

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.

Reseña