Benutzer: Gast  Login
Wenn Sie Schwierigkeiten haben, das Dokument zu öffnen, versuchen Sie auch bitte diesen Link
Originaltitel:
Formalizing Graph Theory and Planarity Certificates
Übersetzter Titel:
Formalisierung von Graphentheorie und Planaritätszertifikaten
Autor:
Noschinski, Lars
Jahr:
2016
Dokumenttyp:
Dissertation
Fakultät/School:
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.
WWW:
https://mediatum.ub.tum.de/?id=1278868
Eingereicht am:
03.11.2015
Mündliche Prüfung:
13.04.2016
Dateigröße:
1031941 bytes
Seiten:
121
Urn (Zitierfähige URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20160413-1278868-1-2
Letzte Änderung:
23.06.2016
 BibTeX