A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL
Wenda Li, Grant Olney Passmore, Lawrence Charles Paulson · arXiv (Cornell University) · 2015
We present a complete, certificate-based decision procedure for first-order univariate polynomial problems in Isabelle. It is built around an executable function to decide the sign of a univariate polynomial at a real algebraic point. The procedure relies on no trusted code except for Isabelle's kernel and code generation. This work is the first step towards integrating the MetiTarski theorem prover into Isabelle.