Formal verification of semi-algebraic sets and real analytic functions

Abstract

Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts appear 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 predictable 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 way that a real analytic function behaves in a neighborhood around a point where the function meets the boundary of a semi-algebraic set is described and verified. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, the behavior around the boundary of a semi-algebraic set can be very different.