14 "Sum_of_Squares/positivstellensatz_tools.ML" |
14 "Sum_of_Squares/positivstellensatz_tools.ML" |
15 "Sum_of_Squares/sos_wrapper.ML" |
15 "Sum_of_Squares/sos_wrapper.ML" |
16 begin |
16 begin |
17 |
17 |
18 text {* |
18 text {* |
19 In order to use the method sos, call it with @{text "(sos |
19 Proof method sos invocations: |
20 remote_csdp)"} to use the remote solver. Or install CSDP |
20 \begin{itemize} |
21 (https://projects.coin-or.org/Csdp), configure the Isabelle setting |
21 |
22 @{text CSDP_EXE}, and call it with @{text "(sos csdp)"}. By |
22 \item remote solver: @{text "(sos remote_csdp)"} |
23 default, sos calls @{text remote_csdp}. This can take of the order |
23 |
24 of a minute for one sos call, because sos calls CSDP repeatedly. If |
24 \item local solver: @{text "(sos csdp)"} |
25 you install CSDP locally, sos calls typically takes only a few |
25 |
26 seconds. |
26 The latter requires a local executable from |
27 sos generates a certificate which can be used to repeat the proof |
27 https://projects.coin-or.org/Csdp and the Isabelle settings variable |
28 without calling an external prover. |
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. |
29 *} |
39 *} |
30 |
40 |
31 setup Sum_of_Squares.setup |
41 setup Sum_of_Squares.setup |
32 setup SOS_Wrapper.setup |
42 setup SOS_Wrapper.setup |
33 |
43 |