Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem
Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre
teoría de grafos titulado Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem.
Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).
Su resumen es
The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chro- matic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a standard textbook proof and use this to explore the use of the probabilistic method in a theorem prover.
El trabajo se presentó en el ITP 2012 (Interactive Theorem Proving).
El código de las correspondientes teorías en Isabelle se encuentra aquí.