sos documentation
authornipkow
Wed Jul 29 12:12:01 2009 +0200 (2009-07-29)
changeset 32270615c524bd9e4
parent 32269 b642e4813e53
child 32271 378ebd64447d
sos documentation
NEWS
     1.1 --- a/NEWS	Wed Jul 29 09:06:49 2009 +0200
     1.2 +++ b/NEWS	Wed Jul 29 12:12:01 2009 +0200
     1.3 @@ -18,6 +18,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New proof method "sos" (sum of squares) for nonlinear real arithmetic
     1.8 +(originally due to John Harison). It requires Library/Sum_Of_Squares.
     1.9 +It is not a complete decision procedure but works well in practice
    1.10 +on quantifier-free real arithmetic with +, -, *, ^, =, <= and <,
    1.11 +i.e. boolean combinations of equalities and inequalities between
    1.12 +polynomials. It makes use of external semidefinite programming solvers.
    1.13 +For more information and examples see Library/Sum_Of_Squares.
    1.14 +
    1.15  * Set.UNIV and Set.empty are mere abbreviations for top and bot.  INCOMPATIBILITY.
    1.16  
    1.17  * More convenient names for set intersection and union.  INCOMPATIBILITY: