Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
Journal of Automated Reasoning
MetadataShow full item record
Li, W., Passmore, G., & Paulson, L. (2017). Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. Journal of Automated Reasoning https://doi.org/10.1007/s10817-017-9424-6
We 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 certiﬁcates, separating solving from verifying: eﬃcient 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 eﬃcacy of this approach, in many cases yielding orders of magnitude improvements over previous methods.
interactive theorem proving, Isabelle/HOL, decision procedure, cylindrical algebraic decomposition
The 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].
Embargo Lift Date
External DOI: https://doi.org/10.1007/s10817-017-9424-6
This record's URL: https://www.repository.cam.ac.uk/handle/1810/267061