author | nipkow |

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

changeset 32271 | 378ebd64447d |

parent 32270 | 615c524bd9e4 |

child 32274 | e7f275d203bc |

sos comments modified

1.1 --- a/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 12:12:01 2009 +0200 1.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Jul 29 12:13:21 2009 +0200 1.3 @@ -1,22 +1,22 @@ 1.4 (* Title: Library/Sum_Of_Squares 1.5 Author: Amine Chaieb, University of Cambridge 1.6 + 1.7 +In order to use the method sos, call it with (sos remote_csdp) to use the remote solver 1.8 +or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path, 1.9 +and call it with (sos csdp). By default, sos calls remote_csdp. This can take of the order 1.10 +of a minute for one sos call, because sos calls CSDP repeatedly. 1.11 +If you install CSDP locally, sos calls typically takes only a few seconds. 1.12 + 1.13 *) 1.14 1.15 header {* A decision method for universal multivariate real arithmetic with addition, 1.16 multiplication and ordering using semidefinite programming*} 1.17 + 1.18 theory Sum_Of_Squares 1.19 imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *) 1.20 uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML" 1.21 begin 1.22 1.23 -(* Note: 1.24 - 1.25 -In order to use the method sos, call it with (sos remote_csdp) to use the remote solver 1.26 -or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path, 1.27 -and call it with (sos csdp) 1.28 - 1.29 -*) 1.30 - 1.31 (* setup sos tactic *) 1.32 setup SosWrapper.setup 1.33