A modular, efficient formalisation of real algebraic numbers
Change log
Authors
Li, W
Paulson, LC
Abstract
This paper presents a construction of the real algebraic numbers with executable arithmetic operations in Isabelle/HOL. Instead of verified resultants, arithmetic operations on real algebraic numbers are based on a decision procedure to decide the sign of a bivariate polynomial (with rational coefficients) at a real algebraic point. The modular design allows the safe use of fast external code. This work can be the basis for decision procedures that rely on real algebraic numbers.
Description
Keywords
Real algebraic geometry, Isabelle/HOL, Decision procedure
Journal Title
CPP 2016 - Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2016
Conference Name
CPP 2016: Certified Proofs and Programs
Journal ISSN
Volume Title
Publisher
ACM
Publisher DOI
Sponsorship
Engineering and Physical Sciences Research Council (EP/I011005/1)
The CSC Cambridge International Scholarship is generously funding Wenda Li’s Ph.D. course.