| author | wenzelm |
| Mon Dec 28 17:43:30 2015 +0100 (2015-12-28) | |
| changeset 61952 | 546958347e05 |
| parent 60500 | 903bb1495239 |
| child 69605 | a96320074298 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/Library/Sum_of_Squares.thy
2 Author: Amine Chaieb, University of Cambridge
3 Author: Philipp Meyer, TU Muenchen
4 *)
6 section \<open>A decision procedure for universal multivariate real arithmetic
7 with addition, multiplication and ordering using semidefinite programming\<close>
9 theory Sum_of_Squares
10 imports Complex_Main
11 begin
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"
18 end