The complexity of theorem-proving procedures
The work
| Authors | Stephen A. Cook |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1971 |
| Citekey | cook1971complexity |
Where it appeared
| Published in | Proceedings of the Third Annual ACM Symposium on Theory of Computing |
|---|---|
| Publisher | Association for Computing Machinery |
| Pages | 151--158 |
Identifiers
| DOI | 10.1145/800157.805047 |
|---|---|
| OpenAlex | W2036265926 |
Access
| Landing page | https://doi.org/10.1145/800157.805047 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/800157.805047 |
Abstract
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.
A copy is held
pdf, 3.0 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-23 14:12 UTC |
Filed under
Cite it as
@inproceedings{cook1971complexity,
title = {The complexity of theorem-proving procedures},
author = {Stephen A. Cook},
year = {1971},
booktitle = {Proceedings of the Third Annual ACM Symposium on Theory of Computing},
publisher = {Association for Computing Machinery},
pages = {151--158},
doi = {10.1145/800157.805047},
}
This record lives at https://refs.drheap.org/cook1971complexity/ and will keep doing so.