Stephen A. Cook

Distinguished University Professor
Department of Computer Science
University of Toronto
Toronto, Canada M5S 3G4

Tel: (416) 978-5183
sacook [at] cs [dot] toronto [dot] edu

I am a member of the Theory Group in the Computer Science Department.

Bio

Picture

BOOK IN PROGRESS WITH PHUONG NGUYEN
ALMOST COMPLETE DRAFT: September 2, 2008
Logical Foundations of Proof Complexity

PAPERS

SLIDES FOR LECTURES

MY CURRENT PhD STUDENTS:

Akitoshi Kawamura
Kaveh Ghasemloo
Dai Tri Man Le
Lila Fontes

MY CURRENT MSc STUDENTS:

Dustin Wehr

MY RECENT PhD's:

Steven Perron
Mark Braverman
Phuong Nguyen
Alan Skelley
Tsuyoshi Morioka
Antonina Kolokolova
Michael Soltys
Valentine Kabanets

COURSE WEB SITES AND COURSE NOTES

• CSC365H Enriched Computational Complexity and Computability, Winter, 2009

• CSC438H/2404H Computability and Logic, Fall, 2008.

• CSC2429H Fall 2007 Introduction to Bounded Arithmetic and Propositional Translations.
  

• CSC2429H Winter 2002 Proof Complexity and Bounded Arithmetic.
  This site includes a pointer to course notes.

• Lectures 4 and 5 for CSC2409S 1973 The notes for my Lecture 4 introduce Method I, a precursor for clause learning for SAT solvers, and my Lecture 5 introduces the propositional pigeonhole clauses (attributed to Karp), together with empirical results on the number of resolvents needed by Method I to generate a resolution refutation. The title of that course was "Logic and Mechanical Proof Procedures".

SOME PAPERS and REVIEWS

Postscript files for the following papers are available:

• Pebbles and Branching Programs for Tree Evaluation, Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, Dustin Wehr. Draft manuscript, 45 pages. (Part of this will appear in MFCS 2009.) ps file pdf file

• 2008 CRM-Fields-PIMS Prize: Allan Borodin, by Stephen Cook. Le Bulletin du CRM, Vol 14 No 1 (Spring 2008), pp 5--8,22. ps file

• Relativizing Small Complexity Classes and their Theories, Klaus Aehlig, Stephen Cook, and Phuong Nguyen. CSL 2007. LNCS 4646 (2007), pp 374--388. Slightly expanded 18 page version ps file

• The Complexity of Proving the Discrete Jordan Curve Theorem, Phuong Nguyen and Stephen Cook. LICS 2007, pp 245--256. ps file for April, 2007 version

• Consequences of the Provability of NP subset P/poly, Stephen Cook and Jan Krajicek. Manuscript pp 1--27, August, 2006, ps file Appears in J. Symbolic Logic (72,4), Dec. 2007, pp. 1353--1371.

• Comments on Beckmann's Uniform Reducts, Stephen Cook. arXiv manuscript cs.CC/0601086 January, 2006.

• Computing over the Reals: Foundations for Scientific Computing, Mark Braverman and Stephen Cook. Notices of the AMS 53,3 (March 2006), pp 318--329. arXiv manuscript cs.CC/0509042 Sept, 2005.

• A Note on the Lengths of G0 Proofs, Stephen Cook. Manuscript pp 1--3, December, 2004. Click here for the postscript file.

• Theories for Complexity Classes and their Propositional Translations, Stephen Cook. In ``Complexity of computations and proofs'', Jan Krajicek, ed., Quaderni di Matematica, 2003, pp 175--227. (This volume appeared March, 2005.) Click here for the postscript file.

• Quantified Propositional Calculus and a Second-Order Theory for NC1, Stephen Cook and Tsuyoshi Morioka. Archive for Mathematical Logic Vol 44 No. 6 (Aug 2005) pp 711-749. Click here for a link to the journal, and here for the postscript file of a preprint.

• The strength of replacement in weak arithmetic, Stephen Cook and Neil Thapen. Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp 256--264. Click here for the postscript file. To appear in TOCL (ACM Transactions on Computational Logic)

• A Second-Order Theory for NL, Stephen Cook and Antonina Kolokolova. Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp 398--407. Click here for the postscript file.

• Theories for TC0 and other Small Complexity Classes, Phuong Nguyen and Stephen Cook. LMCS 2,1 (2006) (Logical Methods in Computer Science) Special Issue: Selected Papers of LICS 2004.

• The Proof Complexity of Linear Algebra, Michael Soltys and Stephen Cook. Annals of Pure and Applied Logic 130 (2004), 277-323. Click here for the postscript file for the manuscript.

• The Importance of the P versus NP Question, Stephen Cook. JACM 50, 1, 2003 (50th Anniversary Issue), pp 27-29. Click here for the postscript file.

• A Complete Axiomatization for Blocks World, Stephen Cook and Yongmei Liu. J. Logic Computat. Vol 13, No. 4 pp 581--594. Click here for a .ps preprint. A preliminary verions appears in Seventh International Symposium on Artificial Intelligence and Mathematics, January, 2002. Click here for the postscript file on the conference web site.

• The Optimal Location of Replicas in a Network Using a READ-ONE-WRITE-ALL Policy, Stephen A. Cook, Jan Pachl, and Irwin Pressman. Distributed Computing (2002), 15: 57-66 (copyright Springer-Verlag). Click here for the postscript file.

• A Second-order System for Polytime Reasoning Based on Gradel's Theorem, Stephen Cook and Antonina Kolokolova. APAL 124 (2003) 193-231. Click here for a preprint. An early version is in Proceedings Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS '01) 2001, 177--186. Click here for the postscript file of a 33 page version appearing as ECCC report number TR01-024 (January, 2001).

• Efficiently Approximable Real-Valued Functions, Valentine Kabanets, Charles Rackoff, and Stephen A. Cook. ECCC Report No. 34(2000). Click here for the postscript file.

• The P versus NP Problem, Stephen Cook, April, 2000. Manuscript prepared for the Clay Mathematics Institute for the Millennium Prize Problems (revised November, 2000). Click here for the postscript file. This paper is also available from the Clay Mathematics Institute.

• The Relative Complexity of NP Search Problems (with Beame, Edmonds, Impagliazzo, and Pitassi). STOC 95. Click here for the journal version: JCSS 57, 3-19 (1998).

• Boolean Programs and Quantified Propositional Proof Systems (with Michael Soltys). Bulletin of the Section of Logic, University of Lodz, Department of Logic, Vol 28 No. 3 (1999) pp 119--129. Click here for the postscript file.

• An Exponential Lower Bound for the Size of Monotone Real Circuits, Armin Haken and Stephen A. Cook. FOCS 95. Click here for the journal version: JCSS 58, 326-335 (1999).

• A Tight Relationship between Generic Oracles and Type-2 Complexity Theory (with Russell Impagliazzo and Tomoyuki Yamakami). Information and Computation 137,2, 1997, pp159-170. Click here for postscript file.

• Finding Hard Instances of the Satisfiability Problem: A Survey (with David Mitchell). DIMACS Series in Discrete Math. and Theoretical Computer Science,35, 1997, pp1-17. Click here for postscript file.

• Relating the Provable Collapse of P to NC1 and the Power of Logical Theories. DIMACS Series in Discrete Math. and Theoretical Computer Science, 39, 1998. Click here for postscript file.

• Review of three papers relating the collapse of the polynomial hierarchy to the collapse of bounded arithmetic. Click here for postscript file.

• Functional Interpretations of Feasibly Constructive Arithmetic, Stephen Cook and Alasdair Urquhart. Annals of Pure and Applied Logic 63 (1993) 103-200. Click here for the postscript file.

• A New Recursion-Theoretic Characterization of the Polytime Functions (with Stephen Bellantoni). Computational Complexity 2 (1992), pp97-110. Click here for a .pdf file.

• A Taxonomy of Problems with Fast Parallel Algorithms. Information and Control 64 (1985) pp 2-22. Click here for a pdf file of a scanned version.

• A Time-Space Tradeoff for Sorting on a General Sequential Model of Computation (with Allan Borodin). SIAM J. Computing Vol 11 No. 2 (1982) pp 287--297. Click here for a scanned .pdf file.

• Storage Requirements for Deterministic Polynomial Time Recognizable Languages (with Ravi Sethi). JCSS 13, 1, 1976. Click here for a scanned .pdf file.

• The Complexity of Theorem Proving Procedures. Proceedings Third Annual ACM Symposium on Thoery of Computing, May 1971, pp 151-158. Click pdf.gz for a compressed pdf file of a scanned version. Click here for a pdf file of a retyped version due to Tim Rohls.

• Chapter III of my 1966 PhD thesis "On the Minimum Computation Time of Functions". Click here for a scanned version, thanks to D. J. Bernstein.

• Slides for talk "Pebbles and Branching Programs" , presented May 30, 2009 on the occasion of Les Valiant's 60th birthday celebration.

• Slides for Lectures ``Formal Reasoning Using Low-Complexity Concepts'' given at the Jan Krajicek's Fall School, Prague, Sept 22-26, 2008.

  • Overview
  • The Theory V0 and the Vi Hierarchy
  • Theories for AC0(2) and other Classes
  • The Vi and TVi Hierarchies and the Quantified Propositional Calculus

• Slides for talk "Bounded Reverse Mathematics", presented at CiE 2007, Siena, Italy

• Slides for talk "Capturing Complexity Classes by their Reasoning Power", presented at workshop "New Directions in Proof Complexity", Newton Institute, April, 2006.

• Slides for Tutorial "How to Associate Propositional Proof Systems and Theories with Complexity Classes", Logic Colloquium 2002, Muenster, August, 2002.

  • Part I: Second Order Bounded Theories

  • Part II: Free-Cut Free Proofs and Witnessing Theorems

  • Part III: Translating Combinatorial Theorems to Propositional Proofs

• Slides for Edinburgh talk "A Survey of Complexity Classes and their Associated Propositional Proof Systems and Theories, and a Proof System for Log Space", presented at the ICMS Workshop "Circuit and Proof Complexity", Edinburgh, October, 2001.

• Slides for talk at Fields Institute Feb, 2001 "Zambella's Model-Theoretic Proof of the Buss Witnessing Theorem"