User: Guest  Login
If you experience problems opening the document, please try this link.
Original title:
Formalizing Graph Theory and Planarity Certificates
Translated title:
Formalisierung von Graphentheorie und Planaritätszertifikaten
Author:
Noschinski, Lars
Year:
2016
Document type:
Dissertation
Faculty/School:
Fakultät für Informatik
Advisor:
Nipkow, Tobias (Prof., Ph.D.)
Referee:
Nipkow, Tobias (Prof., Ph.D.); Mehlhorn, Kurt (Prof. Dr.)
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik; MAT Mathematik
Keywords:
graph theory,directed graphs,planarity,program verification,proof assistant,Isabelle,HOL,probabilistic method
Translated keywords:
Graphentheorie, gerichtete Graphen, Planarität, Programmverifikation, Theorembeweiser, Isabelle, HOL, probabilistische Methode
TUM classification:
DAT 706d; DAT 540d
Abstract:
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.
Translated abstract:
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
Date of submission:
03.11.2015
Oral examination:
13.04.2016
File size:
1031941 bytes
Pages:
121
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20160413-1278868-1-2
Last change:
23.06.2016
 BibTeX