Verifying nonlinear real formulas via sums of squares

John Harrison.

Proceedings of TPHOLs 2007, the 20th International Conference on Theorem Proving in Higher Order Logics. Springer LNCS vol. 4732, pp. 102-118, 2007.

Abstract:

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.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-sos,
        author          = "John Harrison",
        title           = "Verifying nonlinear real formulas via sums of 
                           squares",
        editor          = "Klaus Schneider and Jens Brandt",
        booktitle       = "Proceedings of the 20th International Conference on
                           Theorem Proving in Higher Order Logics,  
                           TPHOLs 2007",
        address         = "Kaiserslautern, Germany",
        year            = 2007,
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 4732,
        pages           = "102--118"}