Graph Theory. 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.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Doczkal, Christian; Pous, Damien: Graph theory in Coq: minors, treewidth, and isomorphisms (2020)
- Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
- Noschinski, Lars: A graph library for Isabelle (2015)
- Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)