# HG changeset patch
# User nipkow
# Date 1248862321 -7200
# Node ID 615c524bd9e4dfde6b8f4e75d649b5384ac5fbdc
# Parent b642e4813e538fe3adbcbfc4dd593a481307d5b7
sos documentation
diff -r b642e4813e53 -r 615c524bd9e4 NEWS
--- a/NEWS Wed Jul 29 09:06:49 2009 +0200
+++ b/NEWS Wed Jul 29 12:12:01 2009 +0200
@@ -18,6 +18,14 @@
*** HOL ***
+* New proof method "sos" (sum of squares) for nonlinear real arithmetic
+(originally due to John Harison). It requires Library/Sum_Of_Squares.
+It is not a complete decision procedure but works well in practice
+on quantifier-free real arithmetic with +, -, *, ^, =, <= and <,
+i.e. boolean combinations of equalities and inequalities between
+polynomials. It makes use of external semidefinite programming solvers.
+For more information and examples see Library/Sum_Of_Squares.
+
* Set.UNIV and Set.empty are mere abbreviations for top and bot. INCOMPATIBILITY.
* More convenient names for set intersection and union. INCOMPATIBILITY: