\documentclass[a4paper]{article}
\usepackage{amssymb}
\pagestyle{empty}
\hoffset=-40pt
\voffset=-20pt
\textwidth 15.3cm
\textheight 22cm % to fit our printers
\begin{document}
\begin{center}{\huge On the complexity of propositional calculus}\end{center}
\begin{center}{\large Pavel Pudl\'{a}k (Prague)}\end{center}
\bigskip

There are several reasons for studying the
complexity of propositional calculus. Firstly, the set of
satisfiable formulas is $\cal NP$-complete, thus ${\cal
NP}=co\cal NP$ is equivalent to the existence of a proof system
(in a general sense) in which every tautology has a proof of at
most polynomial length. There are also connections to
computational complexity problems from cryptography.  Secondly,
lower bounds on the lengths of proofs in particular proof
systems give independence results for fragments arithmetic.
Thirdly, there are quite a few methods in mathematics, mainly in
combinatorial optimization, which can be interpreted as
particular propositional proof systems. It is interesting to
compare their strength and in some cases it is possible to prove
that they are not polynomially bounded (e.g., cutting planes
proofs in integer linear programming).

The most successful general method of proving lower bounds on
the lengths of propositional proofs is based on a property of
some systems called {\em effective interpolation}. This means
that the circuit complexity of interpolating boolean functions
$f(x)$ of an implication $\phi(x,y)\to\psi(x,z)$ can be bounded
by a polynomial in the length of a proof of the implication.
This method has limited applications, apparently it cannot be
used for strong systems, but for several proof systems it gives
reductions to known lower bounds in boolean complexity.

This research leads to natural problems concerning the lengths of
proofs in nonclassical logics, where even less is known than in
the classical case. In particular we would like to find more
than polynomial lower bounds for monotone and intuitionistic
logics. 

\end{document}