A De­ci­sion Pro­ce­dure for Uni­vari­ate Real Poly­no­mi­als in Isa­belle/​HOL

by Manuel Eberl

In: Proceedings of CPP 2015

DOI:

Abstract:

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)

@inproceedings{eberl15cpp,
  author = "Eberl, Manuel",
  title = "A Decision Procedure for Univariate Real Polynomials in {I}sabelle/{HOL}",
  booktitle = "Certified Programs and Proofs, {CPP} 2015",
  year = "2015",
  isbn = "978-1-4503-3296-5",
  pages = "75--83",
  numpages = "9",
  doi = "10.1145/2676724.2693166",
  publisher = "ACM"
}

Download BibTeX (342 Bytes)

(The final publication is available at ACM)