Mauricio Ayala-Rincon: Mechanizing Combinatorial Applications of Compactness
Sprache des Titels:
Englisch
Original Kurzfassung:
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."
Forschungs-