In his "Feasibly Constructive Proofs and the Propositional Calculus" paper published in 1975, he introduced the equational theory PV (standing for Polynomial-time Verifiable) to formalize the notion of proofs using only polynomial-time concepts. He made another major contribution to the field in his 1979 paper, joint with his student Robert A. Reckhow, "The Relative Efficiency of Propositional Proof Systems", in which they formalized the notions of p-simulation and efficient propositional proof system, which started an area now called propositional proof complexity. They proved that the existence of a proof system in which every true formula has a short proof is equivalent to NP = coNP. Cook co-authored a book with his student Phuong The Nguyen in this area titled "Logical Foundations of Proof Complexity".