--- a/NEWS Wed Jul 29 16:42:47 2009 +0200
+++ b/NEWS Wed Jul 29 16:43:02 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:
--- a/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 16:42:47 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 16:43:02 2009 +0200
@@ -1,22 +1,22 @@
(* Title: Library/Sum_Of_Squares
Author: Amine Chaieb, University of Cambridge
+
+In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
+or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
+and call it with (sos csdp). By default, sos calls remote_csdp. This can take of the order
+of a minute for one sos call, because sos calls CSDP repeatedly.
+If you install CSDP locally, sos calls typically takes only a few seconds.
+
*)
header {* A decision method for universal multivariate real arithmetic with addition,
multiplication and ordering using semidefinite programming*}
+
theory Sum_Of_Squares
imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML"
begin
-(* Note:
-
-In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
-or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
-and call it with (sos csdp)
-
-*)
-
(* setup sos tactic *)
setup SosWrapper.setup