Reseña: Graph theory

Se ha publicado un nuevo artículo de razonamiento formalizado en Isabelle/HOL titulado Graph theory.

Su autor es Lars Noschinski (de la Univrsidad Técnica de Munich).

Su resumen es

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.

Definitions and nomenclature are based on Digraphs: Theory, algorithms and applications (by J. Bang-Jensen and G. Gutin).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.