The paper by Stephen A. Cook explores the complexity of theorem-proving procedures, focusing on the problem of determining whether a given propositional formula is a tautology. Cook introduces the concept of polynomial reducibility, where one problem can be solved deterministically in polynomial time if an oracle is available for solving another problem. He defines the polynomial degree of difficulty for sets of strings and shows that the problem of determining tautologyhood has the same polynomial degree as the problem of determining graph isomorphism and subgraph inclusion. The paper also discusses the complexity of proof procedures for the predicate calculus, proposing a measure of efficiency based on the Herbrand theorem. Theorems 1 and 2 provide evidence that determining tautologyhood is a challenging task, and theorems 3 and 4 offer insights into the efficiency of proof procedures. The paper concludes with a discussion on the limitations and potential improvements in complexity theory and the need for better complexity measures in mechanical theorem proving.The paper by Stephen A. Cook explores the complexity of theorem-proving procedures, focusing on the problem of determining whether a given propositional formula is a tautology. Cook introduces the concept of polynomial reducibility, where one problem can be solved deterministically in polynomial time if an oracle is available for solving another problem. He defines the polynomial degree of difficulty for sets of strings and shows that the problem of determining tautologyhood has the same polynomial degree as the problem of determining graph isomorphism and subgraph inclusion. The paper also discusses the complexity of proof procedures for the predicate calculus, proposing a measure of efficiency based on the Herbrand theorem. Theorems 1 and 2 provide evidence that determining tautologyhood is a challenging task, and theorems 3 and 4 offer insights into the efficiency of proof procedures. The paper concludes with a discussion on the limitations and potential improvements in complexity theory and the need for better complexity measures in mechanical theorem proving.