author | nipkow |

Wed Jul 29 12:12:01 2009 +0200 (2009-07-29) | |

changeset 32270 | 615c524bd9e4 |

parent 32269 | b642e4813e53 |

child 32271 | 378ebd64447d |

sos documentation

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: