A modular, efficient formalisation of real algebraic numbers
View / Open Files
Publication Date
2016-01-18Journal Title
CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs
Publisher
Association for Computing Machinery
Pages
66-75
Language
English
Type
Conference Object
Metadata
Show full item recordCitation
Li, W., & Paulson, L. (2016). A modular, efficient formalisation of real algebraic numbers. CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 66-75. https://doi.org/10.1145/2854065.2854074
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.
Keywords
real algebraic geometry, Isabelle/HOL, decision procedure
Sponsorship
The CSC Cambridge International Scholarship is generously funding Wenda Li’s Ph.D. course.
Funder references
EPSRC (EP/I011005/1)
Identifiers
External DOI: https://doi.org/10.1145/2854065.2854074
This record's URL: https://www.repository.cam.ac.uk/handle/1810/253716
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved