Benutzer: Gast  Login
Originaltitel:
A Verified ODE Solver and Smale's 14th Problem 
Übersetzter Titel:
Ein Verifizierter GDGL-Löser und Smales 14. Problem 
Jahr:
2018 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Tucker, Warwick (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Theorem Prover, Isabelle, HOL, ODE, Rigorous Numerics, Lorenz Attractor 
TU-Systematik:
DAT 706d; DAT 540d 
Kurzfassung:
This dissertation presents a formalization of ordinary differential equations (ODEs) and the verification of rigorous (with guaranteed error bounds) numerical algorithms in the interactive theorem prover Isabelle/HOL. The formalization comprises flow and Poincaré map of dynamical systems. The verified algorithms are based on Runge-Kutta methods and affine arithmetic. They certify numerical bounds for the Lorenz attractor and thereby lift the numerical part of Tucker's proof of Smale's 14th probl...    »
 
Übersetzte Kurzfassung:
Diese Dissertation stellt eine Formalisierung von gewöhnlichen Differentialgleichungen (GDGL) und die Verifikation von rigorosen (mit garantierten Fehlerschranken) numerischen Algorithmen im interaktiven Theorembeweiser Isabelle/HOL vor. Die Formalisierung umfasst Fluss und Poincaré-Abbildung dynamischer Systeme. Die verifizierten Algorithmen basieren auf Runge-Kutta-Verfahren und affiner Arithmetik. Sie zertifizieren numerische Schranken für den Lorenz Attraktor und heben dadurch den numerische...    »
 
Mündliche Prüfung:
09.05.2018 
Dateigröße:
22289865 bytes 
Seiten:
161 
Letzte Änderung:
12.07.2018