Article:
James Aisenberg, Maria Luisa Bonet, Sam Buss
Adrian Crãciun, and Gabriel Istrate
"Short Proofs of the Kneser-Lovász
Coloring Principle"
Information and Computation 261, 2 (2018) 296-310.
Download paper: PDF.
Earlier conference version:
In: Proceeedings 42nd International Colloquium
on Automata, Languages and Programming (ICALP)
Springer-Verlag Lectures in Computer Science 9135,
2015, pp. 44-55
Download ICALP 2015 proceedings version:
PDF.
Abstract: We prove that propositional translations of the Kneser-Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs for all fixed values of k. We present a new counting-based combinatorial proof of the Kneser-Lovász theorem based on the Hilton-Milner theorem; this avoids the topological arguments of prior proofs for all but finitely many base cases. We introduce new "truncated Tucker lemma" principles, which are miniaturizations of the octahedral Tucker lemma. The truncated Tucker lemma implies the Kneser-Lovász theorem. We show that the k=1 case of the truncated Tucker lemma has polynomial size extended Frege proofs.