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).
License
Topics
Session Planarity_Certificates
- Lib
- OptionMonad
- NonDetMonad
- NonDetMonadLemmas
- OptionMonadND
- WP
- OptionMonadWP
- Graph_Genus
- List_Aux
- Executable_Permutations
- Digraph_Map_Impl
- Planar_Complete
- Reachablen
- Permutations_2
- Planar_Subdivision
- Planar_Subgraph
- Kuratowski_Combinatorial
- Simpl_Anno
- Check_Non_Planarity_Impl
- Check_Non_Planarity_Verification
- AutoCorres_Misc
- Setup_AutoCorres
- Check_Planarity_Verification
- Planarity_Certificates