Proving Real-Valued Inequalities by Computation in Isabelle/HOL

In this thesis we present an automatic proof method on real valued formulas. It translates the formulas into interval arithmetic calculations on floating point numbers. The resulting formulas are then evaluated by utilizing the code generator. These computations are entirely verified in Isabelle/HOL itself. To reach that goal, we extend the theory with several missing analytical results about trigono-metrical functions, as well as derivation rules for power series. A major new development are the boundary computations for, pi, sin, cos, arctan, exp and ln. Finally the correctness of these computations is verified in Isabelle/HOL. Acknowledgements I am very grateful to Tobias Nipkow, for introducing me to the field of theorem proving, and for all his advice and support. I also want to thank Amine Chaieb for his advice and for reading draft versions of my thesis. A big thank-you goes to Lukas Bulwahn for giving me lots of advice after reading a draft version and for the interesting cocoa breaks. Florian Haftmann helped me a lot with advice to his code generator framework. Thanks are due to the entire Isabelle group a