summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 32270 | 615c524bd9e4 |

parent 32264 | 0be31453f698 |

child 32326 | 9d70ecf11b7a |

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: