Skip to content (access key 's')
Logo of Technion
Logo of CS Department

The Taub Faculty of Computer Science Events and Talks

Theory Seminar: How to Generalize Descartes' Rule of Signs?
event speaker icon
Pavel Hrubes (University of Calgary)
event date icon
Wednesday, 02.01.2013, 12:30
event location icon
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.