Propositional Proofs in Frege and Extended Frege Systems (Abstract)

摘要

We discuss recent results on the propositional proof complexity of Frege proof systems, including some recently discovered quasipoly-nomial size proofs for the pigeonhole principle and the Kneser-Lovasz theorem. These are closely related to formalizability in bounded arithmetic.