Graph Theory

References

Cite

Share

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 isomor-phisms. This formalization is used to prove characterizations of Euler Trails, Shortest Paths and Kuratowski subgraphs. Definitions and nomenclature are based on [1].