Abstract
This development provides a formalization of directed graphs, supporting (labelled) multi-edges and infinite graphs. A polymorphic edge type allows edges to be treated as pairs of vertices, if multi-edges are not required. Formalized properties are i.a. walks (and related concepts), connectedness and subgraphs and basic properties of isomorphisms.
This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs.
License
Topics
Session Graph_Theory
- Rtrancl_On
- Stuff
- Digraph
- Bidirected_Digraph
- Arc_Walk
- Pair_Digraph
- Digraph_Component
- Vertex_Walk
- Digraph_Component_Vwalk
- Digraph_Isomorphism
- Auxiliary
- Subdivision
- Euler
- Kuratowski
- Weighted_Graph
- Shortest_Path
- Graph_Theory
Used by
- An Axiomatic Characterization of the Single-Source Shortest Path Problem
- Positional Determinacy of Parity Games
- Planarity Certificates
- Combinatorial Design Theory
- Verification of Query Optimization Algorithms
- Expander Graphs
- MLSS Decision Procedure
- Elementary Graph Traversal Algorithms
- Muntac: A Verified Certificate Checker for Timed Automata