Formal Verification of Semi-algebraic Sets and Real Analytic Functions
Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts interact in the study of Differential Equations, where the real analytic solution to a differential equation is known to enter or exit a semi-algebraic set in a predicable way. Motivated to enhance the capability to reason about differential equations in the Prototype Verification System (PVS), a formalization of multivariate polynomials, semi-algebraic sets, and real analytic functions is developed. The favorable way that a real analytic function enters and exits a semi-algebraic set is proven. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, these favorable interactions with semi-algebraic sets may fail.
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:45 - 19:30 | Formalized MathematicsCPP at CPP Chair(s): Amin Timany Aarhus University Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768 | ||
18:45 15mTalk | Formalizing the Ring of Witt VectorsDistinguished Paper Award CPP Pre-print Media Attached | ||
19:00 15mTalk | Formal Verification of Semi-algebraic Sets and Real Analytic Functions CPP J Tanner Slagel NASA Langley Research Center, Lauren White Kansas State University, Aaron Dutle NASA Langley Research Center Pre-print Media Attached | ||
19:15 15mTalk | On the Formalisation of Kolmogorov Complexity CPP Pre-print Media Attached |