summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 29 Jul 2009 12:12:01 +0200 | |

changeset 32270 | 615c524bd9e4 |

parent 32269 | b642e4813e53 |

child 32271 | 378ebd64447d |

sos documentation

--- 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: