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 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:45 - 19:30 | Formalized MathematicsCPP at CPP Chair(s): Amin TimanyAarhus 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 SlagelNASA Langley Research Center, Lauren WhiteKansas State University, Aaron DutleNASA Langley Research Center Pre-print Media Attached | ||
19:15 15mTalk | On the Formalisation of Kolmogorov Complexity CPP Pre-print Media Attached |