A Modular, Efficient Formalisation of Real Algebraic Numbers
This paper shows a construction of 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 at 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.
Mon 18 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
16:00 - 18:00
|A Modular, Efficient Formalisation of Real Algebraic Numbers|
|Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials|
|Formalizing Jordan Normal Forms in Isabelle/HOL|
|Formalization of a Newton series representation of polynomials|