Source / pinned edition
The Complexity of Theorem-Proving Procedures
Source of package cook_levin.sat_np_complete_1971 · Proceedings of STOC 1971, pp. 151-158
- work
- urn:doctrine:cs:cook-levin-1971#COOK_1971
- number
- Proceedings of STOC 1971, pp. 151-158
- kind
- urn:doctrine:cs:cook-levin-1971#treatise
COOK_1971_STOC
- edition
- urn:doctrine:cs:cook-levin-1971#COOK_1971_STOC
- language
- en
- officiality
- official
- materialisation
- PINNED_UNOFFICIAL_COPY
- life cycle
- adopted: 1971-05-03
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| https://www.cs.toronto.edu/~sacook/homepage/1971.pdf | text/plain; charset=utf-8 | sha256:83cb4b12a0f2e44b860fb2be00479a10c84609392720533f02a73d6ecef14928 | 2026-09-17T00:00:00Z |
Fragments — 4
1.corollary · lemma
en · official · sha256:11f1055501288763d9ffb65ab3f4db8a2967f2084b768bd4ae372b0608036662
Corollary: Each of the sets in definitions 1)-5) is P-reducible to {DNF tautologies}.summary · defn · referenced by: 8
en · official · sha256:a0c93a9f1d59bd490595e70d25e823b42dbaee0139e62549e8f49bbf2dd0c865
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 of difficulty as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second.Referencing norms: CookLevinClaim, SatChecker, SatLanguage, SatProblem, sat-checker-checks, sat-checker-poly-certificate, sat-checker-poly-time, sat-has-language
1.theorem1 · lemma · referenced by: 3
en · official · sha256:8d15c46cd0eff6363f6fade2ad46237049ae42e501b35f97b982ae691ef8ada6
Theorem 1: If a set S of strings is accepted by some nondeterministic Turing machine within polynomial time, then S is P-reducible to {DNF tautologies}.Referencing norms: CookProof, cook-proves, sat-np-hard-directly
title · defn · referenced by: 1
en · official · sha256:320529fe13a217a1f87896f0a5e9999e29de0e5b421a32880364f7e6fb1a4f78
The Complexity of Theorem-Proving Procedures
Stephen A. Cook
University of TorontoReferencing norms: CookSource
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.