We prove that the propositional translations of the Kneser-Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs. We present a new counting-based combinatorial proof of the Kneser-Lovász theorem that avoids the topological arguments of prior proofs for all but finitely many cases for each
. We introduce a miniaturization of the octahedral Tucker lemma, called the
truncated Tucker lemma
: it is open whether its propositional translations have (quasi-)polynomial size Frege or extended Frege proofs.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten