ANNOTATED REFERENCES for CSC 2429H

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

COMPLEXITY THEORY

Ding-Zhu Du and Ker-I Ko:  Theory of Computational Complexity.  Wiley, 2000.
This book is the text for CSC 2402H, and chapters 1,3, and 6
provide a good background for 2429.

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.
   
R.B. Bopanna and M. Sipser: The Complexity of Finite Functions.
In Handbook (above), pp757-804.
Good for boolean circuit lower bounds.

R. Greenlaw, H.J. Hoover, W.L. Ruzzo:  Limits to Parallel Computation.
P-Completeness Theory.   1995
   Treats the distinction between the classes P and NC, with lots of
examples.

H. Rose:  Subrecursive Hierarchies.
   Has a proof of Cobham's Theorem.

Martin Davis and Elaine Weyuker:  Computability, Complexity, and
Languages.  1983
    Chapter 3 contains a readable treatment of primitive recursive
functions.

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.

Davis and Weyuker:  (See under Complexity Theory above.)

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, 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.

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:
\begin{verbatim}
             http://euclid.ucsd.edu/~sbuss/
\end{verbatim}

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

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

S. Cook and A. Urquhart:  Functional Interpretations of Feasibly
Constructive Arithmetic.  Annals of Pure and Aplplied Logic 63 (1993),
pp103-200.
    Contains a detailed development of the equational theory PV, in
Section 3 and the Appendix.

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.