Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Американский и канадский учёный в области компьютерных наук, внесший вклад в теорию сложности.
American Canadian computer scientist, contributor to complexity theory
Исследования
Во время своей докторской диссертации Кук работал над сложностью функций, в основном над умножением. В своей основополагающей работе 1971 года «Сложность процедур доказательства теорем» Кук формализовал понятия полиномиального сведения (также известного как сведение Кука) и NP-полноты, и доказал существование NP-полной задачи, показав, что задача выполнимости булевых формул (обычно известная как SAT) является NP-полной. Эта теорема была доказана независимо Леонидом Левиным в Советском Союзе, и поэтому получила название теоремы Кука — Левина. В статье также была сформулирована самая известная проблема в информатике — проблема P против NP. Неформально, вопрос «P против NP» заключается в том, можно ли любую задачу оптимизации, ответы на которую можно эффективно проверить на корректность/оптимальность, решить оптимально с помощью эффективного алгоритма. Учитывая обилие таких задач оптимизации в повседневной жизни, положительный ответ на вопрос «P против NP» вероятно, будет иметь глубокие практические и философские последствия. Кук предполагает, что существуют задачи оптимизации (с легко проверяемыми решениями), которые не могут быть решены эффективными алгоритмами, то есть P не равно NP. Эта гипотеза породила большое количество исследований в теории вычислительной сложности, что значительно улучшило наше понимание внутренней сложности вычислительных задач и того, что можно эффективно вычислить. Тем не менее, эта гипотеза остается открытой и входит в число семи знаменитых задач тысячелетия. В 1982 году Кук получил премию Тьюринга за вклад в теорию сложности. Его цитата гласит:
During his PhD, Cook worked on complexity of functions, mainly on multiplication. In his seminal 1971 paper "The Complexity of Theorem Proving Procedures", Cook formalized the notions of polynomial time reduction (also known as Cook reduction) and NP completeness, and proved the existence of an NP complete problem by showing that the Boolean satisfiability problem (usually known as SAT) is NP complete. This theorem was proven independently by Leonid Levin in the Soviet Union, and has thus been given the name the Cook–Levin theorem. The paper also formulated the most famous problem in computer science, the P vs. NP problem. Informally, the "P vs. NP" question asks whether every optimization problem whose answers can be efficiently verified for correctness/optimality can be solved optimally with an efficient algorithm. Given the abundance of such optimization problems in everyday life, a positive answer to the "P vs. NP" question would likely have profound practical and philosophical consequences. Cook conjectures that there are optimization problems (with easily checkable solutions) that cannot be solved by efficient algorithms, i. e., P is not equal to NP. This conjecture has generated a great deal of research in computational complexity theory, which has considerably improved our understanding of the inherent difficulty of computational problems and what can be computed efficiently. Yet, the conjecture remains open and is among the seven famous Millennium Prize Problems. In 1982, Cook received the Turing Award for his contributions to complexity theory. His citation reads:
«За продвижение нашего понимания сложности вычислений значительным и глубоким образом». Его основополагающая работа «Сложность процедур доказательства теорем», представленная на симпозиуме ACM SIGACT 1971 года по теории вычислений, заложила основы теории NP-полноты. Последующее исследование границ и природы класса NP-полных задач стало одной из самых активных и важных областей исследований в информатике за последнее десятилетие. В своей работе «Доказуемо конструктивные доказательства и пропозициональное исчисление», опубликованной в 1975 году, он представил уравнительную теорию PV (обозначающую «Проверяемое за полиномиальное время»), чтобы формализовать понятие доказательств, использующих только концепции полиномиального времени. Он внес еще один важный вклад в эту область в своей работе 1979 года, совместно со своим студентом Робертом А. Рекхоу, «Относительная эффективность систем доказательства пропозициональных формул», в которой они формализовали понятия p-симуляции и эффективной системы доказательства пропозициональных формул, что положило начало области, теперь называемой сложностью доказательства пропозициональных формул. Они доказали, что существование системы доказательств, в которой каждая истинная формула имеет короткое доказательство, эквивалентно NP = coNP. Кук является соавтором книги со своим студентом Фуонгом Нгуеном в этой области под названием «Логические основы сложности доказательств». Его основными областями исследований являются теория сложности и сложность доказательств, с отступлениями в семантику языков программирования, параллельные вычисления и искусственный интеллект. Другие области, в которые он внес вклад, включают ограниченную арифметику, ограниченную обратную математику, сложность функций более высокого порядка, сложность анализа и нижние оценки в системах доказательства пропозициональных формул.
For his advancement of our understanding of the complexity of computation in a significant and profound way. His seminal paper, The Complexity of Theorem Proving Procedures, presented at the 1971 ACM SIGACT Symposium on the Theory of Computing, laid the foundations for the theory of NP Completeness. The ensuing exploration of the boundaries and nature of NP complete class of problems has been one of the most active and important research activities in computer science for the last decade. In his "Feasibly Constructive Proofs and the Propositional Calculus" paper published in 1975, he introduced the equational theory PV (standing for Polynomial time Verifiable) to formalize the notion of proofs using only polynomial time concepts. He made another major contribution to the field in his 1979 paper, joint with his student Robert A. Reckhow, "The Relative Efficiency of Propositional Proof Systems", in which they formalized the notions of p simulation and efficient propositional proof system, which started an area now called propositional proof complexity. They proved that the existence of a proof system in which every true formula has a short proof is equivalent to NP = coNP. Cook co authored a book with his student Phuong The Nguyen in this area titled "Logical Foundations of Proof Complexity". His main research areas are complexity theory and proof complexity, with excursions into programming language semantics, parallel computation, and artificial intelligence. Other areas that he has contributed to include bounded arithmetic, bounded reverse mathematics, complexity of higher type functions, complexity of analysis, and lower bounds in propositional proof systems.
Некоторые другие вклады
Он назвал класс сложности NC в честь Ника Пиппенгера. Класс сложности SC назван в его честь. Он также ввёл определение класса сложности AC0 и его иерархии AC. По словам Дона Кнута, алгоритм KMP был вдохновлён автоматами Кука для распознавания конкатенированных палиндромов за линейное время.
He named the complexity class NC after Nick Pippenger. The complexity class SC is named after him. The definition of the complexity class AC0 and its hierarchy AC are also introduced by him. According to Don Knuth the KMP algorithm was inspired by Cook's automata for recognizing concatenated palindromes in linear time.
Личная жизнь
Кук живёт с женой в Торонто. У них два сына, один из которых – олимпийский яхтсмен Гордон Кук.
Cook lives with his wife in Toronto. They have two sons, one of whom is Olympic sailor Gordon Cook.