The Taub Faculty of Computer Science Events and Talks

The main open problem in proof complexity is to prove superpolynomial lower bounds for the so-called Frege system, where Frege system is a specific formalization of classical propositional calculus. The same problem can be posed for non-classical logics, and I will discuss two popular examples: intuitionistic and modal logic. Here, one actually can prove exponential lower bounds on lengths of proofs. I will show how to construct this lower bound and discuss connections between proof complexity and circuit complexity.