The study of the complexity of proof systems is fundamental to logic and has a broad range of applications in computer science as well. First, the efficiency of any deduction system is tied to the speed of logical reasoning (e.g., Prolog, Datalog, and many inferencing systems in artificial intelligence). Secondly, the complexity of propositional proof systems is intimately connected to the central question in complexity theory of whether NP equal coNP. Finally, there are links between particular propositional proof systems, systems of arithmetic, and complexity classes. Exploiting these connections, one can apply a whole new range of tools from logic to attack difficult complexity questions (such as P = NP). The basic question in propositional logic to be considered is: How long does a proof of a propositional tautology have to be, as a function of the size of the tautology? The best upper bound for all known proof systems is exponential in the size of the tautology and it is conjectured that a similar lower bound holds. This question is equivalent to whether or not NP = coNP, and while it has been studied extensively for the last 25 years, it is still far from solved. Propositional proof systems can be divided into classes that correspond directly to complexity classes. An approach toward proving NP = coNP is to establish superpolynomial lower bounds for specific proof systems of greater and greater proof strength. Much of this research is aimed at attacking this difficult problem. Another line of research concerns feasible arithmetic (also known as bounded arithmetic) and its connections to propositional proofs and complexity theory. The concept of a feasible proof has been the subject of much research in the last ten years.
