A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL
by Manuel Eberl
In: Proceedings of CPP 2015
DOI:
10.1145/2676724.2693166Abstract:
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.
Download preprint PDF (285 KiB)
BibTeX:
@inproceedings{eberl15cpp,
author = {Eberl, Manuel},
title = {A Decision Procedure for Univariate Real Polynomials in {I}sabelle/{HOL}},
booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs},
series = {CPP '15},
year = {2015},
isbn = {978-1-4503-3296-5},
location = {Mumbai, India},
pages = {75--83},
numpages = {9},
doi = {10.1145/2676724.2693166},
acmid = {2693166},
publisher = {ACM},
address = {New York, NY, USA}
}
(The final publication is available at ACM)