Stephen A. Cook
University Professor Emeritus
Department of Computer Science
University of Toronto
Toronto, Canada M5S 3G4
Tel: (416) 9785183
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
Teaching Fall 2013:
CSC463H
Computational Complexity and Computability
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
SLIDES FOR LECTURES
($100 PRIZE OFFER: See slides for the Princeton Barriers conference)
MY CURRENT PhD STUDENTS:
Kaveh Ghasemloo
Dustin Wehr
(Jointly supervised with Alasdair Urquhart)
Robert Robere
(Jointly supervised with Toni Pitassi)
David Liu
(Jointly supervised with Toni Pitassi)
Venkatesh Medabalimi
MY CURRENT (and one PAST) MSc STUDENTS:
Frank Vanderzwet (Jointly supervised with Toni Pitassi) (Graduated December, 2012)
MY RECENT PhD's:
Dai Tri Man Le
Lila Fontes
(Jointly supervised with Toni Pitassi)
Akitoshi Kawamura
Steven Perron
Click here for
Perron's PhD thesis "Power of NonUniformity in Proof Complexity".
Mark Braverman
Phuong Nguyen
Alan Skelley
Tsuyoshi Morioka
Antonina Kolokolova
Michael Soltys
Valentine Kabanets
COURSE WEB SITES AND COURSE NOTES
 CSC438H/2404H
Computability and Logic, Winter, 2014
 CSC463H
Computational Complexity and Computability, Fall, 2013
 CSC2401S
Introduction to Computational Complexity, Winter, 2013.
 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".
FAMILY LINKS:
Gordon's carbon fibre tube business
Gordon in Globe and Mail
Gordon and Ben sailing off San Diego
2010 49er Worlds Grand Bahama Island Gordon and
Hunter
Close action in Sydney (Gordon and Ben)
James
SLIDES FOR LECTURES
SOME PAPERS and REVIEWS
Postscript or pdf files for the following papers are available
(roughly in reverse chronological order):
 Theories for Subexponentialsize Boundeddepth 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.
arXiv:1208.2721v1 [cs.CC]
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.
arXiv:1204.5508v1 [cs.CC]
April, 2012.
This is an expanded version (submitted) of the conference version
in CSL 2007: LNCS 4646 (2007), pp 374388.
 The Hardness of Being Private. Anil Ada, Arkadev Chattopadhyay,
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 125. 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. 131. 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).
 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. 143
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. 175186.
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 109120.
 2008 CRMFieldsPIMS Prize: Allan Borodin, by Stephen Cook.
Le Bulletin du CRM, Vol 14 No 1 (Spring 2008), pp 58,22.
ps file
 The Complexity of Proving the Discrete Jordan Curve Theorem,
Phuong Nguyen and Stephen Cook.
LICS 2007, pp 245256.
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 127, August, 2006,
ps file
Appears in J. Symbolic Logic (72,4), Dec. 2007, pp. 13531371.
 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 318329.
arXiv manuscript
cs.CC/0509042 Sept, 2005.
 A Note on the Lengths of G0 Proofs,
Stephen Cook. Manuscript pp 13, 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 175227.
(This volume appeared March, 2005.)
Click here for the postscript file.
 Quantified Propositional Calculus and a SecondOrder Theory for NC1,
Stephen Cook and Tsuyoshi Morioka. Archive for Mathematical Logic
Vol 44 No. 6 (Aug 2005) pp 711749.
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 256264.
Click here for the postscript file.
To appear in TOCL
(ACM Transactions on Computational Logic)
 A SecondOrder Theory for NL,
Stephen Cook and Antonina Kolokolova.
Nineteenth Annual IEEE Symposium on Logic in Computer Science
(LICS 2004), pp 398407.
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), 277323. 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 2729. 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 581594.
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
READONEWRITEALL Policy, Stephen A. Cook, Jan Pachl, and Irwin Pressman.
Distributed Computing (2002), 15: 5766 (copyright SpringerVerlag).
Click here
for the postscript file.
 A Secondorder System for Polytime Reasoning Based on Gradel's Theorem,
Stephen Cook and Antonina Kolokolova. APAL 124 (2003) 193231.
Click here for a preprint.
An early version is in Proceedings Sixteenth Annual
IEEE Symposium on Logic in Computer Science (LICS '01) 2001, 177186.
Click here
for the postscript file of a 33 page version appearing as ECCC report
number TR01024 (January, 2001).
 Efficiently Approximable RealValued 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, 319 (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 119129.
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, 326335 (1999).
 A Tight Relationship between Generic Oracles and Type2 Complexity
Theory (with Russell Impagliazzo and Tomoyuki Yamakami). Information
and Computation 137,2, 1997, pp159170. 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, pp117. 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) 103200. Click here
for the postscript file.
 A New RecursionTheoretic Characterization of the Polytime Functions
(with Stephen Bellantoni). Computational Complexity 2 (1992), pp97110.
Click here for a .pdf file.
 Problems Complete for Deterministic Logarithmic Space (with
Pierre McKenzie). Journal of Algorithms 8, 385394 (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 222.
Click here for a
pdf file of a scanned version.
 A TimeSpace Tradeoff for Sorting on a General Sequential
Model of Computation (with Allan Borodin). SIAM J. Computing
Vol 11 No. 2 (1982) pp 287297.
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.
 Time Bounded Random Access Machines (with Robert A. Reckhow).
J. Computer and System Sciences 7, pp 354375 (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 151158.
Click here for a
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 LECTURES (postscript files)

Theories for Subexponentialsize Boundeddepth 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 LowComplexity
Concepts'' given at the Jan Krajicek's
Fall School,
Prague, Sept 2226, 2008.
 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: FreeCut 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 ModelTheoretic Proof of the Buss Witnessing Theorem"