Reseña: A formal proof of Kruskal’s tree theorem in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado A formal proof of Kruskal’s tree theorem in Isabelle/HOL.

Su autor es Christian Sternagel (del JAIST, Japón).

Su resumen es

We give the first formalization of Kruskal’s tree theorem in a proof assistant – the closure of a long-standing challenge. More concretely, we present our Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem. Along the way, we discuss proofs of Dickson’s lemma and Higman’s lemma; and close all gaps in the original proofs.

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