Mechanizing Combinatorial Applications of Compactness
Date: 14/10/2024
Time: 13:30 - 14:30
Time: 13:30 - 14:30
Location: HA 105, RISC, Hagenberg
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 and families of sets) that are available in the Isabelle/AFP library "Compactness Theorem for Propositional Logic and Combinatorial Applications."