src/HOL/Library/Sum_of_Squares.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69605 a96320074298
child 70333 0f7edf0853df
permissions -rw-r--r--
improved code equations taken over from AFP
wenzelm@41474
     1
(*  Title:      HOL/Library/Sum_of_Squares.thy
wenzelm@32949
     2
    Author:     Amine Chaieb, University of Cambridge
wenzelm@32949
     3
    Author:     Philipp Meyer, TU Muenchen
chaieb@31119
     4
*)
chaieb@31119
     5
wenzelm@60500
     6
section \<open>A decision procedure for universal multivariate real arithmetic
wenzelm@60500
     7
  with addition, multiplication and ordering using semidefinite programming\<close>
nipkow@32271
     8
wenzelm@41474
     9
theory Sum_of_Squares
wenzelm@38136
    10
imports Complex_Main
wenzelm@32332
    11
begin
chaieb@31119
    12
wenzelm@69605
    13
ML_file \<open>positivstellensatz.ML\<close>
wenzelm@69605
    14
ML_file \<open>Sum_of_Squares/sum_of_squares.ML\<close>
wenzelm@69605
    15
ML_file \<open>Sum_of_Squares/positivstellensatz_tools.ML\<close>
wenzelm@69605
    16
ML_file \<open>Sum_of_Squares/sos_wrapper.ML\<close>
wenzelm@48891
    17
chaieb@31119
    18
end