TypiCal

In order to prove that a system of real polynomial inequalities has no solution, the usual method is to compute a cylindrical algebraic decomposition (CAD) of that system, which yields a false/true answer - for instance, using Mathematica's Reduce function. CAD implementations, especially those that implement optimizations necessary to go beyond toy examples, are notoriously complex and trusting such a massive amount of code for applications such as proving mathematical theorems or proving safety-critical programs is methodologically disputable. Instead of trusting a complex implementation, or building a certified version thereof, we would prefer the complex algorithm produces an easily checkable "witness" of its answer. For systems of polynomials inequalities, the Positivstellensatz theorems ensure the existence of witnesses made of sums of squares of polynomials. As a particular case, a nonnegative polynomial can often be expressed as a sum of squares of polynomials, and can always be expressed as a quotient of sums of squares of polynomials. Such sums of squares are solutions of a semidefinite programming feasibility problem (that is, given F_0, ..., F_n symmetric matrices, finding y_i such that -F_0 + \sum_i y_i F_i is semidefinite positive, that is, has no negative eigenvalues). Unfortunately, direct application of semidefinite programming numerical methods is only possible if the solution set has nonempty interior. This is not the case in general. We propose a workaround for this problem, based on LLL lattice reduction.