CSC 2429H: Proof Complexity and Bounded Arithmetic
Winter,2002
Click here for the 2005 version of the
course, and a link to the book in progress.
Instructor: Stephen Cook
Office SF 2303C
Tel: (416) 978-5183
email: sacook@cs.toronto.edu
Permanent Times and Location: T 2, F 10 in WB 144
Description
This course develops a three-way connection between complexity classes,
formal theories of arithmetic, and propositional proof systems.
Each of several standard complexity
classes, including AC0, LogSpace, Polytime, and PSPACE has a corresponding
theory formalizing reasoning using concepts in that class, and
corresponding to each theory there is a propositional proof system
representing a nonuniform version of the theory.
Prerequisites
Knowledge of predicate calculus and Peano arithmetic,
including preferably the Godel completeness
and incompleteness theorems, and basic knowledge of complexity,
including complexity classes based on time, space, or Boolean circuit
families. CSC 2404H is perfect
for the logic, and CSC 2401H more than suffices for the complexity theory.
Chapters 1-3 and 6 of ``Theory of Computational Complexity''
by Ding-Zhu Du and Ker-I Ko should suffice for complexity theory.
CSC 2404H 2000 Contains notes on logic
providing a background for the present course.
Text:
Jan Krajicek: Bounded Arithmetic, Propositional Logic, and Complexity
Theory. Cambridge, 1995.
Links to relevant articles and a current course by
Sam Buss
Annotated references
Assigned Exercises
COMPOTSITE COURSE NOTES NOW AVAILABLE
as postscript files (except for final lecture).
Slides for Edinburgh Talk These
slides give the gist of the final course lecture, and were presented at
the ICMS Workshop "Circuit and Proof Complexity", October, 2001.
Course Notes are also available below as a series of postscript files.