Some News on the Proof Complexity of Monotone and Deep Inference Proofs

TI will present a classical result of Atserias, Galesi and Pudlák that (tree-like) monotone proofs (MLK) quasipolynomially simulate nonmonotone proofs (LK) over monotone implications. This has very recently been improved to a polynomial simulation for dag-like MLK, but the question for the tree-like fragment and a subsystem corresponding to minimal deep inference remains open. I will demonstrate some of the structural and logical techniques for reasoning about the complexity of deep inference proofs. In particular, I will present a construction of quasipolynomial-size proofs of the propositional pigeonhole principle in minimal deep inference, using a combination of graph rewriting and counting arguments. Finally I will discuss the structure of the monotone counting formulae used. They are symmetric in a somwhat weak sense (up to a syntactic equivalence relation), and the existence of polynomial-size such formulae would essentially solve the remaining open problems in the area.