14/10/202413:30 - 14:30HA 105, RISC, Hagenberg
Mechanizing Combinatorial Applications of Compactness
I will present details of our formalizations in Isabelle/HOL of applications of the compactness theorem. In particular, I will discuss aspects of our formalizations of proofs of Hall's Theorem, König's Theorem, and de Bruijn-Erdös (k-coloring) Theorem over infinite structures (graphs ...