Planarity Certificates

 

Title: Planarity Certificates
Author: Lars Noschinski
Submission date: 2015-11-11
Abstract: This development provides a formalization of planarity based on combinatorial maps and proves that Kuratowski's theorem implies combinatorial planarity. Moreover, it contains verified implementations of programs checking certificates for planarity (i.e., a combinatorial map) or non-planarity (i.e., a Kuratowski subgraph).
BibTeX:
@article{Planarity_Certificates-AFP,
  author  = {Lars Noschinski},
  title   = {Planarity Certificates},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Planarity_Certificates.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Case_Labeling, Graph_Theory, List-Index, Simpl, Transitive-Closure