From Boolean circuits to theorem proving

The question how difficult it is to prove given theorems in given formal systems arises in many areas. In computational complexity, lower bounds to the size of proofs offer an approach towards the separation of complexity classes. Analysis of proof systems underlying recent SAT solvers provides the main theoretical framework towards understanding the power and limitations of solving. The main part of research in proof complexity has concentrated on proof systems for classical propositional logic. Despite the fact that propositional proof complexity has made enormous progress over the past three decades in showing tight lower and upper bounds for many proof systems, some of strong classical proof systems have resisted all attempts for lower bounds for decades. Never the less, a general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. In the paper we show how relates Boolean circuits and proof systems with respect to complexity, i.e. how ideas and techniques from Boolean circuit complexity applies to propositional proof complexity.