Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Földes–Hammer Characteriza...

Email Gateway (Sep 11 2026 at 19:23):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: The Földes–Hammer Characterization of Split Graphs

Dear all,

I’d like to announce a new AFP entry:

The Földes–Hammer Characterization of Split Graphs
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz

This entry formalizes the classical Földes–Hammer theorem characterizing finite split graphs
as exactly the graphs with no induced copy of 2 K_2, C_4, or C_5.
It builds on the AFP session Undirected_Graph_Theory.

https://isa-afp.org/entries/Foldes_Hammer.html

Enjoy,
René

Last updated: Sep 17 2026 at 22:43 UTC