|
|
Close Help | ||||||||||||||
Lengths of propositional proofs
Jan Krajicek
Two fundamental problems connecting logic and computational complexity theory are:
1. Is there a polynomial time algorithm recognizing the set of satisfiable propositional formulas?
This is the famous "P versus NP" problem of S.Cook. If the answer is negative then it still makes a sense to ask:
2. Is there a propositional calculus admitting short proofs of all tautologies ("short" meaning "of size polynomial in the size of the tautology")?
(This is the "NP versus coNP" problem.)
Both problems are expected to have a negative answer. The negative answer to the second problem implies, in particular, super-polynomial lengths-of-proofs lower bounds for all concrete calculi considered in logic (e.g., resolution or Hilbert-style calculi).
Some such lower bounds have been, in fact, established. The aim of the course is to explain main results and methods (and problems) in this area, with emphasis on topics that appear to me to be stimulating for further research. I shall also treat necessary background from boolean complexity, and some connections to bounded arithmetic.
Brief outline of the course:
- Motivations, bounded arithmetic, complexity theory. Basic definitions.
- Effective interpolation, communication complexity, resolution, cutting planes, discretely ordered modules. Limits of effective interpolation, cryptographic conjectures.
- Constant-depth Frege systems, partial truth assignments, switching lemmas, finite forcing. Pigeonhole principle, counting principles.
- Polynomial rings over finite fields, ideal membership proof systems, Nullstellensatz, polynomial calculus. Ajtai's theorem on definability of solutions of symmetric systems of linear equations.
