Reseña: A graph library for Isabelle

Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A graph library for Isabelle.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

In contrast to other areas of such as analysis, number theory or probability theory, no standard library for graph theory has yet evolved for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general infinite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs.

We use this library to formalize a characterization of Euler Digraphs and a to verify a method of checking Kuratowski subgraphs used in the LEDA library.

El código de la teoría en Isabelle se encuentra aquí.