Stephen A. Cook's paper explores the complexity of theorem-proving procedures, showing that any problem solvable by a polynomial-time bounded nondeterministic Turing machine can be reduced to determining whether a propositional formula is a tautology. This reduction implies that the tautology problem has the same polynomial degree of difficulty as other seemingly complex problems, such as graph isomorphism and subgraph problems. The paper introduces the concept of polynomial reducibility, defining sets as P-reducible if one can be solved in polynomial time using an oracle for the other. It defines the polynomial degree of difficulty (deg(S)) for a set S, and shows that the tautology problem has the same degree as the subgraph problem and other related problems. The paper also discusses the complexity of proof procedures for the predicate calculus, introducing a method to measure the efficiency of such procedures. It defines a function T_Q(k) to measure the efficiency of a procedure for determining unsatisfiability of predicate formulas. Theorems show that T_Q(k) must grow faster than certain functions, indicating the inherent difficulty of these problems. The paper concludes that the tautology problem is a candidate for a set not in L*, suggesting it is a significant challenge in complexity theory. The paper emphasizes the need for a theoretical complexity criterion to evaluate and compare theorem-proving procedures, proposing T_Q(k) as a potential measure, though it acknowledges its limitations.Stephen A. Cook's paper explores the complexity of theorem-proving procedures, showing that any problem solvable by a polynomial-time bounded nondeterministic Turing machine can be reduced to determining whether a propositional formula is a tautology. This reduction implies that the tautology problem has the same polynomial degree of difficulty as other seemingly complex problems, such as graph isomorphism and subgraph problems. The paper introduces the concept of polynomial reducibility, defining sets as P-reducible if one can be solved in polynomial time using an oracle for the other. It defines the polynomial degree of difficulty (deg(S)) for a set S, and shows that the tautology problem has the same degree as the subgraph problem and other related problems. The paper also discusses the complexity of proof procedures for the predicate calculus, introducing a method to measure the efficiency of such procedures. It defines a function T_Q(k) to measure the efficiency of a procedure for determining unsatisfiability of predicate formulas. Theorems show that T_Q(k) must grow faster than certain functions, indicating the inherent difficulty of these problems. The paper concludes that the tautology problem is a candidate for a set not in L*, suggesting it is a significant challenge in complexity theory. The paper emphasizes the need for a theoretical complexity criterion to evaluate and compare theorem-proving procedures, proposing T_Q(k) as a potential measure, though it acknowledges its limitations.