Theory Seminar: How to Generalize Descartes' Rule of Signs?

Speaker:
Pavel Hrubes (University of Calgary)
Date:
Wednesday, 2.1.2013, 12:30
Place:
Taub 201

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.

Back to the index of events