Links

Tools

Export citation

Search in Google Scholar

A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL

Journal article published in 2015 by Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Question mark in circle
Preprint: policy unknown
Question mark in circle
Postprint: policy unknown
Question mark in circle
Published version: policy unknown

Abstract

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. ; Comment: 15 pages