summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Sum_Of_Squares.thy

changeset 32271 | 378ebd64447d |

parent 32268 | d50f0cb67578 |

child 32332 | bc5cec7b2be6 |

--- a/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 12:12:01 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 12:13:21 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