The complexity of theorem-proving procedures
Open accessAbstract
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.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Computational complexity theory can be used to classify types of problems, which makes it somewhat more relevant to the paper's concern.
“That said, computational complexity theory can be used to classify types of problems, which makes it somewhat more relevant to our concern (Cook, 1971; Karp, 1972; Sipser, 2012).”
From Understanding Agent Complexity Through Affordances (2025) · cites this paper as Cook, 1971
Cited by
Sorted by citations
Deep learning in neural networks: an overview
Schmidhuber, J. (2015) · Neural Networks · doi:10.1016/j.neunet.2014.09.003 · Cited by 18,570 · see citing works
The knowledge complexity of interactive proof systems
Goldwasser, S., Micali, S., & Rackoff, C. (1989) · SIAM Journal on Computing · doi:10.1137/0218012 · Cited by 3,285 · see citing works
Valiant, L. G. (1984) · Communications of the ACM · doi:10.1145/1968.1972 · Cited by 3,279 · see citing works
The complexity of computing the permanent
Valiant, L. G. (1979) · Theoretical Computer Science · doi:10.1016/0304-3975(79)90044-6 · Cited by 2,705 · see citing works
Gühne, O., & Tóth, G. (2009) · Physics Reports · doi:10.1016/j.physrep.2009.02.004 · Cited by 2,401 · see citing works
Optimization, approximation, and complexity classes
Papadimitriou, C. H., & Yannakakis, M. (1991) · Journal of Computer and System Sciences · doi:10.1016/0022-0000(91)90023-x · Cited by 1,653 · see citing works
Constructing optimal binary decision trees is NP-complete
Hyafil, L., & Rivest, R. L. (1976) · Information Processing Letters · doi:10.1016/0020-0190(76)90095-8 · Cited by 959 · see citing works
Micali, S. (2000) · SIAM Journal on Computing · doi:10.1137/s0097539795284959 · Cited by 424 · see citing works
Siraichi, M. Y., Santos, V. F. D., Collange, C., & Pereira, F. M. Q. (2018) · Proceedings of the 2018 International Symposium on Code Generation and Optimization · doi:10.1145/3168822 · Cited by 254 · see citing works
Hallucination is Inevitable: An Innate Limitation of Large Language Models
Xu, Z., Jain, S., & Kankanhalli, M. (2024) · arXiv · doi:10.48550/arxiv.2401.11817 · Cited by 180 · see citing works
“Problem 4 Boolean Satisfiability (SAT) [11]: given a formula of m Boolean variables, f returns “yes” if there exists an assignment on these variables which results in the formula to be true and “no” otherwise. a Presburger arithmetic is the first-order theory of natural numbers with addition and…”
BackgroundReachability Deficits in Quantum Approximate Optimization
Akshay, V., Philathong, H., Morales, M. E. S., & Biamonte, J. D. (2020) · Physical Review Letters · doi:10.1103/physrevlett.124.090504 · Cited by 151 · see citing works
Quantum Hamiltonian Complexity
Gharibian, S., Huang, Y., Landau, Z., & Shin, S. W. (2015) · Foundations and Trends® in Theoretical Computer Science · doi:10.1561/0400000066 · Cited by 144 · see citing works
Martinize2 and Vermouth provide a unified framework for molecular topology generation
Kroon, P. C., Grünewald, F., Barnoud, J., van Tilburg, M., Brasnett, C., Souza, P. C., Wassenaar, T. A., & Marrink, S. J. (2025) · eLife · doi:10.7554/elife.90627 · Cited by 124 · see citing works
A cross-disciplinary introduction to quantum annealing-based algorithms
Venegas-Andraca, S. E., Cruz-Santos, W., McGeoch, C., & Lanzagorta, M. (2018) · Contemporary Physics · doi:10.1080/00107514.2018.1450720 · Cited by 83 · see citing works
On the Paradox of Learning to Reason from Data
Zhang, H., Li, L. H., Meng, T., Chang, K.-W., & Broeck, G. V. D. (2022) · arXiv · doi:10.48550/arxiv.2205.11502 · Cited by 58 · see citing works
On the Paradox of Learning to Reason from Data
Zhang, H., Li, L. H., Meng, T., Chang, K.-W., & Van den Broeck, G. (2023) · Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence · doi:10.24963/ijcai.2023/375 · Cited by 58 · see citing works
Higher-order molecular organization as a source of biological function
Gaudelet, T., Malod-Dognin, N., & Pržulj, N. (2018) · Bioinformatics · doi:10.1093/bioinformatics/bty570 · Cited by 46 · see citing works
Babbush, R., Perdomo‐Ortiz, A., O'Gorman, B., Macready, W., & Aspuru‐Guzik, A. (2014) · Advances in Chemical Physics · doi:10.1002/9781118755815.ch05 · Cited by 45 · see citing works
Assessing Solution Quality of 3SAT on a Quantum Annealing Platform
Gabor, T., Zielinski, S., Feld, S., Roch, C., Seidel, C., Neukart, F., Galter, I., Mauerer, W., & Linnhoff-Popien, C. (2019) · Lecture Notes in Computer Science · doi:10.1007/978-3-030-14082-3_3 · Cited by 21 · see citing works
Understanding Agent Complexity Through Affordances
Baker, B., & Roberts, S. (2025) · Minds and Machines · doi:10.1007/s11023-025-09748-7
“That said, computational complexity theory can be used to classify types of problems, which makes it somewhat more relevant to our concern (Cook, 1971; Karp, 1972; Sipser, 2012).”
Evidence of scaling advantage on an NP-complete problem with enhanced quantum solvers
Lu, Q., Wei, S., Li, K., Gao, P., Yan, B., Zheng, M., Zhang, H., Zeng, J., & Long, G.-L. (2026) · Nature Computational Science · doi:10.1038/s43588-026-01007-8 · Cited by 1 · see citing works
“2c. in conjunctive normal form (CNF), as a conjunction of clauses where each clause is a disjunction of three literals, was the first problem proven to be NP-complete by the Cook–Levin theorem 26 .”
- Authors
- Cook, S. A.
- Affiliations
- University of Toronto (CA)
- Corresponding author
- Cook, Stephen A.
- Venue
- Proceedings of the third annual ACM symposium on Theory of computing - STOC '71
- Publisher
- ACM Press
- Published
- 1971
- Pages
- 151-158
- OpenAlex
- W2036265926
- Cited by
- 6,385
- References
- 0
- Citations by year
- 2026: 66 · 2025: 145 · 2024: 158 · 2023: 220 · 2022: 185 · 2021: 263 · 2020: 218 · 2019: 283 · 2018: 245 · 2017: 192 · 2016: 214 · 2015: 238 · 2014: 269 · 2013: 288 · 2012: 217
- FWCI
- 16.06
- Type
- conference paper
- Language
- en
- Open access
- bronze
- doi.org
- Locations
- ACM Symposium on Theory of Computing (STOC) (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Complexity and Algorithms in Graphs
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Advanced Graph Theory Research
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Computability, Logic, AI Algorithms
- Keywords
- theorem proving, computational complexity, polynomial-time reduction, nondeterministic Turing machines, graph isomorphism, subgraph isomorphism, oracle computation
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
