The complexity of theorem-proving procedures

By S. Cook. 1971

It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be “reduced” to the problem of determining whether a given propositional formula is a tautology. Here “reduced” means, roughly speaking, that the first problem can be solved deterministically in polynomial time provided an oracle is available for solving the second. From this notion of reducible, polynomial degrees of difficulty are defined, and it is shown that the problem of determining tautologyhood has the same polynomial degree as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second. Other examples are discussed. A method of measuring the complexity of proof procedures for the predicate calculus is introduced and discussed.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Deep learning in neural networks: An overview (2014, background): “For example, an answer to the famous question of whether P = NP (Cook, 1971; Levin, 1973b) would also set limits for what is achievable by general RL. Comparemore specific limitations, e.g., Blondel and Tsitsiklis (2000), Madani, Hanks, and Condon (2003) and Vlassis, Littman, and Barber (2012).”
Learning a SAT Solver from Single-Bit Supervision (2018, background): “Cook (1971) showed that the problem is NP -complete, which means that searching for any kind of efﬁciently-checkable certiﬁcate in any context can be reduced to ﬁnding a satisfying assignment of a propositional formula.”
Vital nodes identification in complex networks (2016, background): “Cook [190] and Karp [191] introduced the so-called feedback vertex set (FVS) problem in the early 1970s.”
Algorithmic construction of sets for k-restrictions (2006, methodology): “According to the traditional de.nition [Cook 1971], NP is the class of all languages having a polynomially checkable membership proof.”
Learning to Discover Efficient Mathematical Identities (2014, background): “The problem addressed in this paper overlaps with the areas of theorem proving [5, 9, 11], program induction [18, 28] and probabilistic programming [12, 20].”
A survey of computational complexity results in systems and control (2000, methodology): “The ZOIP problem turns out to be a hardest problem within the class NP in the sense that every problem in NP can be reduced to ZOIP, in polynomial time (Cook, 1971).”
The Complexity Era in Economics (2011, background): “12This is linked with the much debated question of P ¼ NP in computational complexity (Cook, 1971; Sipser, 1992), where P represents problems solvable in a time bounded above polynomially, whereas NP is bounded above exponentially or by some other higher form than polynomial.”
Elements of Finite Model Theory (2004, background): “Cook's theorem is from [39] (and is presented in many texts of complexity and computability, e.”
Quantum Computational Complexity (2008, background): “Its proof of completeness can roughly be seen as a quantum analogue of the proof of the Cook–Levin Theorem [40, 75].”
Reducibility Among Combinatorial Problems (1972, background): “Cook’s 1971 paper [1], in which he defined the class NP and showed that propositional satisfiability was an NP-complete problem, brought together for me the two strands of complexity theory and combinatorial optimization.”
MAX k-CUT and approximating the chromatic number of random graphs (2006, background): “As soon as there are clauses with K ≥ 3 variables this problem is NPcomplete [7, 13].”