Repository logo
 

Counting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem

cam.issuedOnline2019-01-14
cam.orpheus.successThu Nov 05 11:53:22 GMT 2020 - Embargo updated
dc.contributor.authorLi, W
dc.contributor.authorPaulson, LC
dc.contributor.orcidPaulson, Lawrence [0000-0003-0288-4279]
dc.date.accessioned2019-01-22T00:30:25Z
dc.date.available2019-01-22T00:30:25Z
dc.date.issued2019
dc.description.abstractMany problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-counting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots. In this paper, we have strengthened the root-counting ability in Isabelle/HOL by first formally proving the Budan-Fourier theorem. Subsequently, based on Descartes' rule of signs and Taylor shift, we have provided a verified procedure to efficiently over-approximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm's theorem. Finally, we combine verified components in the developments above to improve our previous certified complex-root-counting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics.
dc.description.sponsorshipERC Advanced Grant ALEXANDRIA (Project 742178)
dc.identifier.doi10.17863/CAM.35599
dc.identifier.isbn9781450362221
dc.identifier.issn0707-9141
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/288283
dc.language.isoeng
dc.publisherACM
dc.publisher.urlhttp://dx.doi.org/10.1145/3293880.3294092
dc.subjectformal verification
dc.subjecttheorem proving
dc.subjectIsabelle
dc.subjectthe Budan-Fourier theorem
dc.subjectDescartes' rule of signs
dc.subjectcounting polynomial roots
dc.titleCounting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem
dc.typeConference Object
dcterms.dateAccepted2018-11-27
prism.endingPage64
prism.publicationDate2019
prism.publicationNameCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
prism.startingPage52
pubs.conference-finish-date2019-01-15
pubs.conference-nameCPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
pubs.conference-start-date2019-01-14
pubs.funder-project-idEuropean Research Council (742178)
rioxxterms.licenseref.startdate2019-01-14
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.typeConference Paper/Proceeding/Abstract
rioxxterms.versionAM
rioxxterms.versionofrecord10.1145/3293880.3294092

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
1811.11093.pdf
Size:
261.59 KB
Format:
Adobe Portable Document Format
Description:
Accepted version
Licence
http://www.rioxx.net/licenses/all-rights-reserved
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
DepositLicenceAgreementv2.1.pdf
Size:
150.9 KB
Format:
Adobe Portable Document Format