The existence of an optimal propositional proof system is a major open question in proof complexity; many people conjecture that such systems do not exist. Krajicek and Pudlak (1989) show that this question is equivalent to the existence of an algorithm that is optimal on all propositional tautologies. Monroe (2009) ... more >>>