Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL

W Li, G Passmore & Lawrence Paulson
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 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....

This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.