@article{NMD15, author = "Anthony Narkawicz and C{\'{e}}sar Mu{\~{n}}oz and Aaron Dutle", journal={Journal of Automated Reasoning}, doi={10.1007/s10817-015-9320-x}, title={Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on {S}turm's and {T}arski's Theorems}, url={http://dx.doi.org/10.1007/s10817-015-9320-x}, publisher={Springer Netherlands}, keywords={Non-linear arithmetic; Decision procedure; Prototype Verification System (PVS); polynomial inequalities; Sturm's theorem; Tarski's theorem; Automated theorem proving; Interactive Theorem Proving}, pages={285-326}, volume={54}, number={4}, language={English}, year={2015}, issn={0168-7433}, }