Return to Revisions

This is perhaps closer to computational complexity than to logic, but there are many open problems in propositional proof complexity that are analogous to, and have close connections to, well-known open problems in computational complexity. For example, it is widely believed that there are tautologies whose proof in a Frege system is necessarily exponential in size; however, so far, no superpolynomial lower bounds have been proven.