author | immler |
Tue, 15 May 2018 11:33:43 +0200 | |
changeset 68188 | 2af1f142f855 |
parent 60500 | 903bb1495239 |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
41474 | 1 |
(* Title: HOL/Library/Sum_of_Squares.thy |
32949
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32645
diff
changeset
|
2 |
Author: Amine Chaieb, University of Cambridge |
aa6c470a962a
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents:
32645
diff
changeset
|
3 |
Author: Philipp Meyer, TU Muenchen |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
4 |
*) |
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
5 |
|
60500 | 6 |
section \<open>A decision procedure for universal multivariate real arithmetic |
7 |
with addition, multiplication and ordering using semidefinite programming\<close> |
|
32271 | 8 |
|
41474 | 9 |
theory Sum_of_Squares |
38136 | 10 |
imports Complex_Main |
32332 | 11 |
begin |
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
12 |
|
48891 | 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 |
||
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
18 |
end |