Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq/Ssreflect sobre grafos titulado Graph theory in Coq: minors, treewidth, and isomorphisms.

Sus autores son

  • Christian Doczkal (Université Côte d’Azur, Inria Sopia Antipolis Méditerranée, France) y
  • Damien Pous (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France).

Su resumen es

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger’s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

El trabajo se ha publicado en el Journal of Automated Reasoning

El código de las correspondientes teorías se encuentra aquí.