Источник / закреплённая редакция
The Complexity of Theorem-Proving Procedures
Источник пакета cook_levin.sat_np_complete_1971 · Proceedings of STOC 1971, pp. 151-158
- work
- urn:doctrine:cs:cook-levin-1971#COOK_1971
- номер
- Proceedings of STOC 1971, pp. 151-158
- вид
- urn:doctrine:cs:cook-levin-1971#treatise
COOK_1971_STOC
- edition
- urn:doctrine:cs:cook-levin-1971#COOK_1971_STOC
- язык
- en
- официальность
- official
- материализация
- PINNED_UNOFFICIAL_COPY
- жизненный цикл
- adopted: 1971-05-03
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| https://www.cs.toronto.edu/~sacook/homepage/1971.pdf | text/plain; charset=utf-8 | sha256:83cb4b12a0f2e44b860fb2be00479a10c84609392720533f02a73d6ecef14928 | 2026-09-17T00:00:00Z |
Фрагменты — 4
1.corollary · lemma
en · official · sha256:11f1055501288763d9ffb65ab3f4db8a2967f2084b768bd4ae372b0608036662EN
Corollary: Each of the sets in definitions 1)-5) is P-reducible to {DNF tautologies}.summary · defn · на него ссылаются: 8
en · official · sha256:a0c93a9f1d59bd490595e70d25e823b42dbaee0139e62549e8f49bbf2dd0c865EN
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.Ссылаются нормы: CookLevinClaim, SatChecker, SatLanguage, SatProblem, sat-checker-checks, sat-checker-poly-certificate, sat-checker-poly-time, sat-has-language
1.theorem1 · lemma · на него ссылаются: 3
en · official · sha256:8d15c46cd0eff6363f6fade2ad46237049ae42e501b35f97b982ae691ef8ada6EN
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}.Ссылаются нормы: CookProof, cook-proves, sat-np-hard-directly
title · defn · на него ссылаются: 1
en · official · sha256:320529fe13a217a1f87896f0a5e9999e29de0e5b421a32880364f7e6fb1a4f78EN
The Complexity of Theorem-Proving Procedures
Stephen A. Cook
University of TorontoСсылаются нормы: CookSource
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.