Benutzer: Gast  Login
Originaltitel:
Formalizing Graph Theory and Planarity Certificates 
Übersetzter Titel:
Formalisierung von Graphentheorie und Planaritätszertifikaten 
Jahr:
2016 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Mehlhorn, Kurt (Prof. Dr.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik; MAT Mathematik 
Stichworte:
graph theory,directed graphs,planarity,program verification,proof assistant,Isabelle,HOL,probabilistic method 
Übersetzte Stichworte:
Graphentheorie, gerichtete Graphen, Planarität, Programmverifikation, Theorembeweiser, Isabelle, HOL, probabilistische Methode 
TU-Systematik:
DAT 706d; DAT 540d 
Kurzfassung:
This thesis studies the formalization of graphs in the Isabelle/HOL proof assistant. It describes a library for directed graphs and discusses its usage for undirected graphs and certificates of planarity. A new technique for structuring and presenting proof obligations provides a convenient language for program verification. Building on these results, programs checking such planarity certificates are verified. 
Übersetzte Kurzfassung:
Diese Dissertation befasst sich mit der Darstellung von Graphen in dem Theorembeweiser Isabelle/HOL. Sie beschreibt eine Formalisierung gerichteter Graphen und diskutiert die Anwendung auf ungerichtete Graphen und Planaritätszertifikate. Eine neue Technik zur Strukturierung und Präsentation von Beweisen bietet eine geeignete Sprache zur Programmverifikation, die dann auf Programme zur Überprüfung von Planaritätszertifikaten angewendet wird. 
Mündliche Prüfung:
13.04.2016 
Dateigröße:
1031941 bytes 
Seiten:
121 
Letzte Änderung:
23.06.2016