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 Jan
|16:00 - 16:30|
|16:30 - 17:00|
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials
|17:00 - 17:30|
|17:30 - 18:00|