author | wenzelm |
Sun, 06 Jan 2019 15:04:34 +0100 | |
changeset 69605 | a96320074298 |
parent 60500 | 903bb1495239 |
child 70333 | 0f7edf0853df |
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 |
|
69605 | 13 |
ML_file \<open>positivstellensatz.ML\<close> |
14 |
ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close> |
|
15 |
ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close> |
|
16 |
ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close> |
|
48891 | 17 |
|
31119
2532bb2d65c7
A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff
changeset
|
18 |
end |