Verifying Nonlinear Real Formulas Via Sums of Squares

12 years 26 days ago
Verifying Nonlinear Real Formulas Via Sums of Squares
Techniques based on sums of squares appear promising as a general approach to the universal theory of reals with addition and multiplication, i.e. verifying Boolean combinations of equations and inequalities. A particularly attractive feature is that suitable ‘sum of squares’ certificates can be found by sophisticated numerical methods such as semidefinite programming, yet the actual verification of the resulting proof is straightforward even in a highly foundational theorem prover. We will describe our experience with an implementation in HOL Light, noting some successes as well as difficulties. We also describe a new approach to the univariate case that can handle some otherwise difficult examples. 1 Verifying nonlinear formulas over the reals Over the real numbers, there are algorithms that can in principle perform quantifier elimination from arbitrary first-order formulas built up using addition, multiplication and the usual equality and inequality predicates. A classic ...
John Harrison
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Authors John Harrison
Comments (0)