Mauricio Ayala-Rincon: Mechanizing Combinatorial Applications of Compactness

Description

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."

Period	14 Oct 2024
Event type	Guest talk
Location	AustriaShow on map