Stephen A. Cook

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

Tel: (416) 978-5183
sacook [at] cs [dot] toronto [dot] edu
Office: Sandford Fleming 2303C

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

Bio

Picture

2015 Picture

Teaching Winter, 2018: CSC463H Computational Complexity and Computability

Taught Fall, 2017: CSC438F/2404F Computability and Logic

My book with Phuong Nguyen
"LOGICAL FOUNDATIONS OF PROOF COMPLEXITY" (ASL Perspectives in Logic Series)
is now available from Cambridge University Press.
Click here for a list of corrections.
Click here for a partial draft from September 2, 2008.

PAPERS
HISTORIC PUBLICATIONS

SLIDES FOR LECTURES
($100 PRIZE OFFER: See slides for the Princeton Barriers conference)

MY CURRENT PhD STUDENTS:

Robert Robere (Toni Pitassi is his principle advisor.)

MY RECENT PhD's:

Venkatesh Medabalimi
Kaveh Ghasemloo Click here for Kaveh's PhD thesis "Uniformity and Nonuniformity in Proof Complexity".
Dustin Wehr (Jointly supervised with Alasdair Urquhart)
Dai Tri Man Le
Lila Fontes (Jointly supervised with Toni Pitassi)
Akitoshi Kawamura
Steven Perron Click here for Perron's PhD thesis "Power of Non-Uniformity in Proof Complexity".
Mark Braverman
Phuong Nguyen
Alan Skelley
Tsuyoshi Morioka
Antonina Kolokolova
Michael Soltys
Valentine Kabanets

COURSE WEB SITES AND 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".

SLIDES FOR LECTURES

SOME PAPERS and REVIEWS

Postscript or pdf files for the following papers are available (roughly in reverse chronological order):

• Theories for Subexponential-size Bounded-depth Frege Proofs. Kaveh Ghasemloo and Stephen A. Cook. Computer Science Logic (CSL) 2013. DOI: 10.4230/LIPIcs.CSL.2013.296 September, 2013.
• The Complexity of the Comparator Circuit Value Problem. Stephen A. Cook, Yuval Filmus, and Dai Tri Man Le. ACM Transactions on Computation Theory (TOCT) Vol 6, No. 4, Aug, 2014. Almost final ToCT version 13 Aug 2012. This paper is a sequel to the following paper:

• A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem. Dai Tri Man Le, Stephen Cook, and Yuli Ye. CSL 2011 (Computer Science Logic). pdf file (conference version). pdf file (long version).

• Relativizing Small Complexity Classes and their Theories, Klaus Aehlig, Stephen Cook, and Phuong Nguyen.
  Computational Complexity 25 (2016), pp 177-214. See arXiv:1204.5508v1 [cs.CC] for an earlier version (April, 2012), which is an expanded version of the conference version in CSL 2007: LNCS 4646 (2007), pp 374--388.

• The Hardness of Being Private. Anil Ada, Arkadev Chattopadhyay, Stephen Cook, Lila Fontes, Michal Koucky, Toniann Pitassi. CCC 2012. pdf file

• Relativized Propositional Calculus. Stephen Cook. Working paper posted 9 March, 2012, based on my talk at the complexity theory workshop at Oberwolfach, 30 April, 2003. arXiv:1203.2168v1

• Formalizing Randomized Matching Algorithms. Dai Tri Man Le and Stephen A Cook. Logical Methods in Computer Science (LMCS) Vol 8 (3:05) 2012. pp 1-25. An earlier version appeared in LICS 2011.

• Formal Theories for for Linear Algebra. Stephen Cook and Lila Fontes. Logical Methods in Computer Science Vol. 8 (1:25) 2012,pp. 1--31. An early version appeared in Computer Science Logic (CSL) 2010.

• Complexity Theory for Operators in Analysis, Akitoshi Kawamura and Stephen Cook. STOC 2010. pdf file
  Click here for an extended version (September, 2010).

• New Results for Tree Evaluation. Sui Man Chan, James Cook, Stephen Cook, Phuong Nguyen, Dustin Wehr. pdf file
  NOTE: This is unpublished work from 2010 and earlier. Ignore the subtitle ``Not for Distribution.''

• Pebbles and Branching Programs for Tree Evaluation. Stephen Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, Rahul Santhanam. ACM Transactions on Computation Theory (ToCT) (3,2), Jan 2012, pp. 1--43 See correction for a correction to the proof of Theorem 5.15. For an earlier version of the paper, see arXive reference (Parts of this appear in the next two conference papers.)

  Branching Programs for Tree Evaluation. Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, Dustin Wehr. 34th International Symposium, Mathematical Foundations of Computer Science (MFCS 2009), LNCS 5734 (2009), Springer, pp. 175--186.
  ps file pdf file

  Fractional Pebbling and Thrifty Branching Programs, Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, Dustin Wehr. link to FSTTCS 2009 Proceedings pages 109-120.

• 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

• 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 Journal Version ACM ToCL (13,1)

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

• Problems Complete for Deterministic Logarithmic Space (with Pierre McKenzie). Journal of Algorithms 8, 385--394 (1987). Click here for a .pdf file of a scanned copy.

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

• Soundness and Completeness of an Axiom System for Program Verification. SIAM J. compuing Vol 7, No. 1, (1978) pp70 -- 90. Click here for a scanned .pdf file. Click here for a correction.

• The Relative Efficiency of Propositional Proof Systems (with Robert A. Reckhow). J. Symbolic Logic Vol. 44 No. 1 (1979). Click here for a .pdf file.
  Correction: in Corollary 4.7: `if P not= NP' should be 'if coNP not= NP'.

• On the Lengths of Proofs in the Propositional Calculus. This is the 1976 PhD thesis by Robert A. Reckhow. Click here for a .pdf file.

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

• Feasibly Constructive Proofs and the Propositional Calculus. STOC '75 Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, pages 83-97. Click here for the link to the ACM Digital Library.

• Time Bounded Random Access Machines (with Robert A. Reckhow). J. Computer and System Sciences 7, pp 354--375 (1973). 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 here for a pdf file of a scanned version. Click here for a pdf file of a retyped version due to Tim Rohls.

• Characterizations of Pushdown Machines in Terms of Time-Bounded Computers. JACM Volume 18 Issue 1, Jan. 1971, pp 4-18. Click here for the link to the ACM Digital Library.

• A Survey of Classes of Primitive Recursive Functions. Notes for UC Berkeley Math 290, Sec 14, January 1967, including Cobham's class L and Bennett's class (denoted here by L+) of extended positive rudimentary functions. It is noted that the corresponding relations consist of the class now called NP. Click here for a transcribed version, thanks to Bruce Kapron. (This is published as TR17-001 on ECCC)

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

• The Instrinsic Computational Difficulty of Functions, by Alan Cobham. Proc. of the 1964 International Congress for Logic, Methodology, and the Philosophy of Science, North-Holland Publising Co. Amesterdam, pp 24-30. Click here for a scanned .pdf file.

• Degree of difficulty of Computing a Function and a Partial Ordering of Recursive Sets, by Michael Rabin, Hebrew University, 25 April, 1960. Click here for a scanned .pdf file.

• The Complexity of the Comparator Circuit Value Problem (joint with Yuval filmus and Dai Tri Man Le), presented at the Computational Complexity workshop at Banff, July, 2013.

• Theories for Subexponential-size Bounded-depth Frege Proofs (joint with Kaveh Ghasemloo), presented at Turin, CSL 2013.

• The Complexity and Proof Complexity of the Comparator Circuit Value Problem, Invited talk at the workshop ``Limits of Theorem Proving'', Rome, September, 2012.

• Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems, Invited talk, CSL 2012, September, 2012.

• Bounded Reverse Mathematics, Part I of talk presented at Banff Proof Complexity Workshop, October, 2011.

• Formalizing Randomized Matching Algorithms (joint work with Dai Tri Man Le), Part II of talk presented at Banff Proof Complexity Workshop, October, 2011.

• A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem (joint work with Dai Tri Man Le and Yuli Ye), presented at CSL 2011.

• Slides for Math Teachers Talk, presented Aug 17, 2011.

• Slides for talk "Branching Programs: Avoiding Barriers", presented Aug 27, 2009 at the Barriers Workshop in Princeton. See the last slide for a $100 Prize offer.

• 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"