“The Complexity of Theorem-Proving Procedures” is the 1971 paper by Stephen A. Cook that founded the theory of NP-completeness. It was presented at the Third Annual ACM Symposium on the Theory of Computing (STOC) and runs roughly eight pages; a scanned copy is hosted on Cook’s own University of Toronto homepage, and a retyped, text-searchable transliteration is mirrored at Stanford.
The paper’s central result is a reduction theorem. Cook proved that any recognition problem solvable by a polynomial-time-bounded nondeterministic Turing machine can be reduced to the question of whether a given propositional formula is a tautology (equivalently, whether its negation is satisfiable). In other words, satisfiability captures the full difficulty of the entire class NP.
This was the first demonstration that a single, concrete problem could be universal for NP - the property now called NP-completeness. The paper effectively introduced the P versus NP question and gave researchers a tool, polynomial-time reduction, for proving that other problems share satisfiability’s hardness.
The impact was immediate and lasting. Within a year Richard Karp used Cook’s framework to show that twenty-one classic combinatorial problems are NP-complete, and the paper is regarded as one of the most influential results in the history of computer science. Cook received the 1982 Turing Award largely for this contribution.