equal
deleted
inserted
replaced
6 header {* A decision method for universal multivariate real arithmetic with addition, |
6 header {* A decision method for universal multivariate real arithmetic with addition, |
7 multiplication and ordering using semidefinite programming *} |
7 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 uses |
|
12 "positivstellensatz.ML" |
|
13 "Sum_of_Squares/sum_of_squares.ML" |
|
14 "Sum_of_Squares/positivstellensatz_tools.ML" |
|
15 "Sum_of_Squares/sos_wrapper.ML" |
|
16 begin |
11 begin |
|
12 |
|
13 ML_file "positivstellensatz.ML" |
|
14 ML_file "Sum_of_Squares/sum_of_squares.ML" |
|
15 ML_file "Sum_of_Squares/positivstellensatz_tools.ML" |
|
16 ML_file "Sum_of_Squares/sos_wrapper.ML" |
17 |
17 |
18 text {* |
18 text {* |
19 Proof method sos invocations: |
19 Proof method sos invocations: |
20 \begin{itemize} |
20 \begin{itemize} |
21 |
21 |