Show simple item record

dc.contributor.authorLi, Wen
dc.contributor.authorPassmore, Gen
dc.contributor.authorPaulson, Lawrenceen
dc.date.accessioned2017-09-06T12:58:23Z
dc.date.available2017-09-06T12:58:23Z
dc.identifier.issn0168-7433
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/267061
dc.description.abstractWe present a proof procedure for univariate real polynomial problems in Isabelle/HOL. The core mathematics of our procedure is based on univariate cylindrical algebraic decomposition. We follow the approach of untrusted certificates, separating solving from verifying: efficient external tools perform expensive real algebraic computations, producing evidence that is formally checked within Isabelle’s logic. This allows us to exploit highly-tuned computer algebra systems like Mathematica to guide our procedure without impacting the correctness of its results. We present experiments demonstrating the efficacy of this approach, in many cases yielding orders of magnitude improvements over previous methods.
dc.description.sponsorshipThe first author was funded by the China Scholarship Council, via the CSC Cambridge Scholarship programme. The development of MetiTarski was supported by the Engineering and Physical Sciences Research Council [Grant Numbers EP/I011005/1, EP/I010335/1].
dc.language.isoenen
dc.publisherSpringer
dc.rightsAttribution 4.0 Internationalen
dc.rightsAttribution 4.0 Internationalen
dc.rightsAttribution 4.0 Internationalen
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/en
dc.subjectinteractive theorem provingen
dc.subjectIsabelle/HOLen
dc.subjectdecision procedureen
dc.subjectcylindrical algebraic decompositionen
dc.titleDeciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOLen
dc.typeArticle
prism.publicationNameJournal of Automated Reasoningen
dc.identifier.doi10.17863/CAM.12118
dcterms.dateAccepted2017-07-27en
rioxxterms.versionofrecord10.1007/s10817-017-9424-6en
rioxxterms.versionVoRen
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/en
rioxxterms.licenseref.startdate2017-07-27en
dc.contributor.orcidPaulson, Lawrence [0000-0003-0288-4279]
dc.identifier.eissn1573-0670
rioxxterms.typeJournal Article/Reviewen
cam.issuedOnline2017-08-08en
cam.orpheus.successThu Jan 30 13:00:02 GMT 2020 - The item has an open VoR version.*
rioxxterms.freetoread.startdate2100-01-01


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International