Мартин Дэвид Дэвис (8 марта 1928 г. — 1 января 2023 г.) — американский математик и учёный-компьютерщик, внёсший вклад в области теории вычислимости и математической логики . Его работа над десятой проблемой Гильберта привела к теореме MRDP . Он также развил модель Пост-Тьюринга и стал соавтором алгоритма Дэвиса-Патнэма-Логемана-Лавленда (DPLL) , который является основополагающим для решателей булевой выполнимости .
Дэвис получил премию Лероя П. Стила , премию Шовена (совместно с Рубеном Хершем ) и премию Лестера Р. Форда . Он был членом Американской академии искусств и наук и членом Американского математического общества .
Родители Дэвиса были еврейскими иммигрантами в США из Лодзи , Польша, и поженились после того, как снова встретились в Нью-Йорке. Дэвис родился в Нью-Йорке 8 марта 1928 года. Он вырос в Бронксе , где его родители поощряли его получить полное образование. [1] [2] Он окончил престижную Высшую школу наук Бронкса в 1944 году и получил степень бакалавра по математике в Сити-колледже в 1948 году и степень доктора философии в Принстонском университете в 1950 году. [3] Его докторская диссертация под названием « О теории рекурсивной неразрешимости » была написана под руководством американского математика и ученого-компьютерщика Алонзо Чёрча . [1] [2] [4]
Во время исследовательской стажировки в Иллинойсском университете в Урбана-Шампейн в начале 1950-х годов он присоединился к Лаборатории систем управления и стал одним из первых программистов ORDVAC . [ 1] Позже он работал в Bell Labs и RAND Corporation , прежде чем присоединиться к Нью-Йоркскому университету . [1] Во время своего пребывания в Нью-Йоркском университете он помог создать университетский факультет компьютерных наук. Он вышел на пенсию из Нью-Йоркского университета в 1996 году. [3] [1] Позже он был приглашенным преподавателем в Калифорнийском университете в Беркли . [5]
Дэвис впервые работал над десятой проблемой Гильберта во время своей докторской диссертации, работая с Алонзо Чёрчем. Теорема, сформулированная немецким математиком Давидом Гильбертом , задаёт вопрос: существует ли алгоритм, который может решить, разрешимо ли уравнение, имея диофантово уравнение ? [1] В диссертации Дэвиса была выдвинута гипотеза о том, что проблема неразрешима. В 1950-х и 1960-х годах Дэвис вместе с американскими математиками Хилари Патнэм и Джулией Робинсон добился прогресса в решении этой гипотезы. Доказательство гипотезы было окончательно завершено в 1970 году работой русского математика Юрия Матиясевича . Это привело к появлению теоремы MRDP или DPRM , названной в честь Дэвиса, Патнэма, Робинсона и Матиясевича. [1] Описывая проблему, Дэвис ранее упоминал, что он находил ее «неотразимо соблазнительной», когда был студентом, и позднее она постепенно стала его «пожизненной одержимостью». [6]
Дэвис сотрудничал с Патнэмом, Джорджем Логеманном и Дональдом В. Лавлендом в 1961 году, чтобы представить алгоритм Дэвиса – Патнэма–Логеманна–Лавленда (DPLL) , который был полным алгоритмом поиска с возвратом для определения выполнимости пропозициональных логических формул в конъюнктивной нормальной форме , т. е. для решения проблемы CNF-SAT . [7] Алгоритм был усовершенствованием более раннего алгоритма Дэвиса–Патнэма , который был процедурой на основе резолюции , разработанной Дэвисом и Патнэмом в 1960 году. [8] [9] Алгоритм является основополагающим в архитектуре быстрых решателей булевой выполнимости. [6]
В дополнение к своей работе по теории вычислимости , Дэвис также внес значительный вклад в области вычислительной сложности и математической логики . [1] [6] [10] Дэвис также был известен своей моделью пост-тьюринговых машин . [3]
В 1974 году Дэвис получил премию Лестера Р. Форда за свои разъяснительные работы, связанные с его работой над десятой проблемой Гильберта, [2] [11] , а в 1975 году он получил премию Лероя П. Стила и премию Шовена (совместно с Рубеном Хершем ). [12] Он стал членом Американской академии искусств и наук в 1982 году, [2] а в 2013 году он был выбран в качестве одного из первых членов Американского математического общества . [13]
Книга Дэвиса 1958 года «Вычислимость и неразрешимость» считается классикой в теоретической информатике , а его книга 2000 года «Универсальный компьютер» прослеживает эволюцию и историю вычислений, начиная с работ Готфрида Вильгельма Лейбница и Алана Тьюринга . [1] Его книга «Неразрешимое» , первое издание которой было опубликовано в 1965 году, представляла собой сборник неразрешимых задач и вычислимых функций . [6]
Дэвис был женат на Вирджинии Уайтфорд Палмер, художнице по текстилю. Пара познакомилась во время своего пребывания в районе Урбана-Шампейн и впоследствии поженилась в 1951 году. [14] : 8 У них было двое детей. [3] Пара жила в Беркли, Калифорния , после его выхода на пенсию. [1]
Дэвис умер 1 января 2023 года в возрасте 94 лет. [15] Его жена умерла в тот же день несколько часов спустя. [16]
Книги
Статьи
