Мартин Дэвис: Жизнь и вклад в математику и информатику
Martin Davis (mathematician)
Мартин Дэвис (1928-2023) – амер. математик и информатик, внес вклад в теорию вычислимости и мат. логику. Решение 10-й проблемы Гильберта, алгоритм DPLL.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Американский математик (1928–2023)
American mathematician (1928–2023)
Мартин Дэвид Дэвис (8 марта 1928 – 1 января 2023) – американский математик и учёный в области информатики, внесший вклад в теорию вычислимости и математическую логику. Его работа над десятой проблемой Гильберта привела к теореме MRDP. Он также развивал модель Поста – Тьюринга и был одним из разработчиков алгоритма Дэвиса – Путнама – Логемана – Ловеленда (DPLL), являющегося основой для решателей задач булевой выполнимости. Дэвис был удостоен премии Лероя П. Стила, премии Шовене (совместно с Рубеном Хершем) и премии Лестера Р. Форда. Он был членом Американской академии искусств и наук и членом Американского математического общества.
Martin David Davis (March 8, 1928 – January 1, 2023) was an American mathematician and computer scientist who contributed to the fields of computability theory and mathematical logic. His work on Hilbert's tenth problem led to the MRDP theorem. He also advanced the Post–Turing model and co developed the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, which is foundational for Boolean satisfiability solvers. Davis won the Leroy P. Steele Prize, the Chauvenet Prize (with Reuben Hersh), and the Lester R. Ford Award. He was a fellow of the American Academy of Arts and Sciences and a fellow of the American Mathematical Society.
Ранние годы и образование
Родители Дэвиса были еврейскими иммигрантами из Лодзи, Польша, и поженились после повторной встречи в Нью-Йорке. Дэвис родился в Нью-Йорке 8 марта 1928 года. Он вырос в Бронксе, где его родители поощряли его к получению полноценного образования. Он окончил престижную Бронксскую среднюю школу науки в 1944 году, а затем получил степень бакалавра математики в Сити-колледже в 1948 году и степень доктора философии в Принстонском университете в 1950 году. Его докторская диссертация под названием «О теории рекурсивной неразрешимости» была написана под руководством американского математика и ученого в области компьютерных наук Алонзо Черча.
Davis's parents were Jewish immigrants to the United States from Łódź, Poland, and married after they met again in New York City. Davis was born in New York City on March 8, 1928. He grew up in the Bronx, where his parents encouraged him to obtain a full education. He graduated from the prestigious Bronx High School of Science in 1944 and went on to receive his bachelor's degree in mathematics from City College in 1948 and his PhD from Princeton University in 1950. His doctoral dissertation, entitled On the Theory of Recursive Unsolvability, was supervised by American mathematician and computer scientist Alonzo Church.
Академическая карьера
Во время работы в качестве научного сотрудника в Университете Иллинойса в Урбана-Шампейн в начале 1950-х годов он присоединился к Лаборатории систем управления и стал одним из первых программистов ЭВМ ORDVAC.
During a research instructorship at the University of Illinois at Urbana Champaign in the early 1950s, he joined the Control Systems Lab and became one of the early programmers of the ORDVAC.
Десятая проблема Гильберта
Дэвис впервые занялся десятой проблемой Гильберта в своей диссертации под руководством Алонзо Черча. Теорема, сформулированная немецким математиком Давидом Гильбертом, ставит вопрос: существует ли алгоритм, определяющий, имеет ли данное диофантово уравнение решение?
Davis first worked on Hilbert's tenth problem during his PhD dissertation, working with Alonzo Church. The theorem, as posed by the German mathematician David Hilbert, asks a question: given a Diophantine equation, is there an algorithm that can decide if the equation is solvable?
Другие взносы
В 1961 году Дэвис сотрудничал с Путнамом, Джорджем Логеманом и Дональдом В. Ловеландом для разработки алгоритма Дэвиса–Путнама–Логемана–Ловеланда (DPLL) – полного алгоритма поиска с возвратом для определения выполнимости формул пропозициональной логики в конъюнктивной нормальной форме, то есть для решения задачи CNF SAT. Алгоритм стал усовершенствованием более раннего алгоритма Дэвиса–Путнама, основанного на методе резолюций, разработанном Дэвисом и Путнамом в 1960 году. Этот алгоритм является основополагающим в архитектуре современных быстрых решателей задач булевой выполнимости. Дэвис также известен своей моделью машин Поста–Тьюринга. В 1975 году он был удостоен премии Лероя П. Стила и премии Шовене (совместно с Рубеном Хершем). В 1982 году он стал членом Американской академии искусств и наук.
Davis collaborated with Putnam, George Logemann, and Donald W. Loveland in 1961 to introduce the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, which was a complete, backtracking based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i. e. for solving the CNF SAT problem. The algorithm was a refinement of the earlier Davis–Putnam algorithm, which was a resolution based procedure developed by Davis and Putnam in 1960. The algorithm is foundational in the architecture of fast Boolean satisfiability solvers. Davis was also known for his model of Post–Turing machines. and in 1975 he won the Leroy P. Steele Prize and the Chauvenet Prize (with Reuben Hersh). He became a fellow of the American Academy of Arts and Sciences in 1982,
Книга Дэвиса «Вычислимость и неразрешимость» (1958) считается классикой теоретической информатики, а его книга «Универсальный компьютер» (2000) прослеживает эволюцию и историю вычислительной техники, начиная с работ Готфрида Вильгельма Лейбница и Алана Тьюринга. У них было двое детей. Дэвис скончался 1 января 2023 года в возрасте 94 лет. Его жена умерла в тот же день, спустя несколько часов.
Davis's 1958 book Computability and Unsolvability is considered a classic in theoretical computer science, while his 2000 book The Universal Computer traces the evolution and history of computing starting including works of Gottfried Wilhelm Leibniz and Alan Turing. They had two children. Davis died on January 1, 2023, at age 94. His wife died the same day several hours later.