ANNOTATED REFERENCES for CSC 2429H

BASIC REFERENCES:

Jan Krajicek:  Bounded Arithmetic, Propositional Logic, and
Complexity Theory.  Cambridge, 1995.

Sam Buss, ed.  Handbook of Proof Theory.  Elsevier, 1998.
Chapter I provides a good treatment of LK and cut elimination,
and Chapter II is a good survey of bounded arithmetic.
(See 2429 course web page for a link to these chapters.)

COMPLEXITY THEORY

Sanjeev Arora and Boaz Barak:  Complexity Theore:  A Modern Approach.
(Draft available on the Web)
A good general introduction.  Chapter 6 defines the class AC0
(important to this course).

Neil Immerman:  Descriptive Complexity.  Springer, 1999
Chapters 1 and 2 are  useful background.
We need Theorem 5.30:  FO = ALogTime, where FO (First Order) is
a finite model-theoretic characterization of uniform AC0,
and  ALogTime (Alternating Log Time) is a characterization of the same
thing in terms of alternating Turing machines.

David Johnson:  A Catalog of Complexity Classes.  In Handbook of
Theoretical Computer Science, Vol A, J. Van Leeuwen, Ed., 1990, pp67-162.

Complexity Zoo (on the Web via google) contains references to
hundreds of complexity classes.
   
H. Rose:  Subrecursive Hierarchies.
   Has a proof of Cobham's Theorem.

John Savage:  Models of Computation.  1998
This undergraduate text has lots of material, including explicit
constructions of boolean circuits for arithmetic, etc.

--------------------------------------
LOGIC

H.B. Enderton:  A Mathematical Introduction to Logic.  1970
   A readable undergraduate text.

Kenneth McAloon:  Models of Arithmetic and Complexity Theory.
In Studies in Complexity Theory, R.V.Book, Ed., 1986, pp119-222.
   Introduction to nonstandard models of arithmetic.

Petr Hajek and Pavel Pudlak:  Metamathematics of First-Order Arithmetic.
1993
    Contains much detailed information on Peano Arithmetic and its
subtheories.  Analyzes complexity of$\Delta_0$ relations.

Sam Buss:  Bounded Arithmetic.  1986
   Introduces the hierachy $S_2$ of theories of bounded arithmetic.
   Full of information.

Sam Buss:  Various survey papers.  See his home page:

G. Takeuti:  Proof Theory.  1987
   Gives a proof of the cut elimination theorem.

T. Pitassi et al:  Propositional Proof Complexity:  Past, Present,
and Future, 2001. A good survey paper available from Toni Pitassi's
home page.

A. Urquhart:  The Complexity of Propositional Proofs.  Bull. Symbolic
Logic 1,4, 1995, pp425-467.
   Another good survey paper.

Domenico Zambella: Notes on Polynomially Bounded Arithmetic.
JSL 61 (3), 1996 pp 942-966.  A nice model theoretic treatment
of second order systems of arithmetic.  Our $\V0$ and $\VV$ 
are close to systems presented here.

Paul Beame and Toni Pitassi:  Simplified and Improved Resolution
Lower Bounds.  37th FOCS, 1996.  Contains a slick proof of the
exponential lower bound for the Pigeon Hole Principle, etc.