Кіріспе

Американдық математик (1928–2023)

Мартин Дэвид Дэвис (8 наурыз 1928 – 1 қаңтар 2023) – американдық математик және компьютерлік ғалым, есептеу теориясы және математикалық логика салаларына үлес қосып, Гилберттің оныншы мәселесі бойынша жүргізген жұмысы MRDP теоремасына әкелді. Ол сондай-ақ Пост–Тьюринг моделін дамытып, Бульдік қанағаттандыруды шешетін программалардың негізі болған Дэвис–Путнам–Логеман–Ловеланд (DPLL) алгоритмін бірлесіп жасады. Дэвис Лерой П. Стил сыйлығын, Рубен Хершпен бірге Шоувене сыйлығын және Лестер Р. Форд сыйлығын жеңіп алды. Ол Америка өнер және ғылым академиясының және Америка математикалық қоғамының мүшесі болды.

Ерте өмір және білім

Дэвистің ата-анасы Польшаның Лодзь қаласынан АҚШ-қа көшіп келген еврей иммигранттары еді және олар Нью-Йорк қаласында қайта кездескеннен кейін үйленді. Дэвис 1928 жылдың 8 наурызында Нью-Йорк қаласында дүниеге келді. Ол Бронкста өсті, онда оның ата-анасы толық білім алуға ынталандырды. Ол 1944 жылы беделді Бронкс ғылым орта мектебін бітіріп, 1948 жылы Сити колледжінде математика мамандығы бойынша бакалавр дәрежесін, ал 1950 жылы Принстон университетінде докторлық дәрежесін алды. Оның докторлық диссертациясы "Рекурсивті шешілмейтін мәселелер теориясы" деп аталып, американдық математик және компьютер ғалымы Алонзо Черч басшылығымен жазылған.

Академиялық мансап

1950 жылдардың басында Иллинойс университетінің Урбана-Шампейн қаласындағы ғылыми-зерттеу оқытушысы қызметін атқағанда, ол Басқару жүйелері зертханасына қатысып, ORDVAC компьютерінің алғашқы бағдарламашыларының бірі болды.

Хилберттің оныншы мәселесі

Дэвис алғаш рет Хилберттің оныншы проблемасы бойынша докторлық диссертациясында Алонзо Черчпен бірге жұмыс істеді. Немец математигі Дэвид Гилберт қойған теорема мына сұраққа жауап іздейді: берілген Диофанти теңдеуі шешімге ие ме екенін анықтайтын алгоритм бар ма?

Басқа салымдар

1961 жылы Дэвис Путнам, Джордж Логеман және Дональд В. Лавлендпен бірлесіп, Дэвис–Путнам–Логеман–Лавленд (DPLL) алгоритмін ұсынды. Бұл алгоритм – конъюнктивті нормалды формадағы логикалық формулалардың қанағаттандырылуын анықтауға арналған толық, кері іздеуге негізделген іздеу алгоритмі, яғни CNF SAT мәселесін шешуге арналған. Алгоритм 1960 жылы Дэвис және Путнам жасаған шешімге негізделген процедура болған бұрынғы Дэвис–Путнам алгоритмінің жетілдірілген нұсқасы еді. Алгоритм жылдам бульдік қанағаттандырушыларды (Boolean satisfiability solvers) құру архитектурасының негізі болып табылады. Дэвис сонымен қатар Пост–Тьюринг машиналарының моделін жасауымен де белгілі болды. 1975 жылы ол Лерой П. Стил сыйлығы мен Шовене сыйлығын (Рубен Хершпен бірге) жеңіп алды. 1982 жылы Америка өнер және ғылым академиясының мүшесі атанды.

Дэвистің 1958 жылғы «Есептеу мүмкіндігі және шешілмейтін мәселелер» кітабы теориялық компьютерлік ғылымдағы классикалық туынды саналады, ал 2000 жылғы «Жалпы компьютер» кітабы Готфрид Вильгельм Лейбниц және Алан Тьюрингтің еңбектерінен бастап, есептеудің эволюциясы мен тарихын баяндайды. Олардың екі баласы болды. Дэвис 2023 жылдың 1 қаңтарында 94 жасында дүние салды. Оның әйелі де сол күні бірнеше сағаттан кейін қайтыс болды.