1 (* Title: HOL/Library/Sum_of_Squares.thy |
1 (* Title: HOL/Library/Sum_of_Squares.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 Author: Philipp Meyer, TU Muenchen |
3 Author: Philipp Meyer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* A decision method for universal multivariate real arithmetic with addition, |
6 header {* A decision procedure for universal multivariate real arithmetic |
7 multiplication and ordering using semidefinite programming *} |
7 with addition, multiplication and ordering using semidefinite programming *} |
8 |
8 |
9 theory Sum_of_Squares |
9 theory Sum_of_Squares |
10 imports Complex_Main |
10 imports Complex_Main |
11 begin |
11 begin |
12 |
12 |
13 ML_file "positivstellensatz.ML" |
13 ML_file "positivstellensatz.ML" |
14 ML_file "Sum_of_Squares/sum_of_squares.ML" |
14 ML_file "Sum_of_Squares/sum_of_squares.ML" |
15 ML_file "Sum_of_Squares/positivstellensatz_tools.ML" |
15 ML_file "Sum_of_Squares/positivstellensatz_tools.ML" |
16 ML_file "Sum_of_Squares/sos_wrapper.ML" |
16 ML_file "Sum_of_Squares/sos_wrapper.ML" |
17 |
17 |
18 text {* |
|
19 Proof method sos invocations: |
|
20 \begin{itemize} |
|
21 |
|
22 \item remote solver: @{text "(sos remote_csdp)"} |
|
23 |
|
24 \item local solver: @{text "(sos csdp)"} |
|
25 |
|
26 The latter requires a local executable from |
|
27 @{url "https://projects.coin-or.org/Csdp"} and the Isabelle settings variable |
|
28 variable @{text ISABELLE_CSDP} pointing to it. |
|
29 |
|
30 \end{itemize} |
|
31 |
|
32 By default, method sos calls @{text remote_csdp}. This can take of |
|
33 the order of a minute for one sos call, because sos calls CSDP |
|
34 repeatedly. If you install CSDP locally, sos calls typically takes |
|
35 only a few seconds. |
|
36 |
|
37 The sos method generates a certificate which can be used to repeat |
|
38 the proof without calling an external prover. |
|
39 *} |
|
40 |
|
41 end |
18 end |