Джон Алан Робинсон
Джон Алан Робинсон | |
---|---|
Рожденный | Галифакс, Западный Йоркшир , Великобритания | 9 марта 1930 г.
Умер | 5 августа 2016 г. Портленд, Мэн , США | (86 лет)
Альма-матер | Кембриджский университет Университет Орегона Принстонский университет |
Известный | принцип разрешения , унификация |
Награды | Премия AMS Milestone 1985 г., премия старшего ученого Гумбольдта 1995 г., премия Эрбрана 1996 г. |
Научная карьера | |
Учреждения | Сиракузский университет |
Диссертация | Причинность, вероятность и показания (1957) |
Докторантура | Карл Хемпель [1] |
Джон Алан Робинсон (9 марта 1930 — 5 августа 2016) — философ, математик и учёный-компьютерщик . Он был почетным профессором Сиракузского университета .
Основной вклад Алана Робинсона — в создание основ автоматизированного доказательства теорем . Его алгоритм объединения устранил один источник комбинаторного взрыва в средствах доказательства разрешения ; он также подготовил почву для парадигмы логического программирования , в частности для языка Пролог . Робинсон получил в 1996 году премию Эрбрана за выдающийся вклад в автоматизированное мышление .
Жизнь
[ редактировать ]Робинсон родился в Галифаксе , Йоркшир, Англия, в 1930 году. [2] и уехал в Соединенные Штаты в 1952 году, получив степень по классической литературе в Кембриджском университете . Он изучал философию в Университете Орегона, а затем перешел в Принстонский университет , где получил докторскую степень по философии в 1956 году. Затем он работал в DuPont аналитиком по исследованию операций , где изучил компьютерное программирование и сам изучил математику . В 1961 году он переехал в Университет Райса , проводя лето в качестве приглашенного исследователя в отделе прикладной математики Аргоннской национальной лаборатории . В 1967 году он перешел в Сиракузский университет в качестве заслуженного профессора логики и информатики. [3] и стал почетным профессором в 1993 году. [4]
Именно в Аргонне Робинсон заинтересовался автоматизированным доказательством теорем и разработал унификацию и принцип разрешения. Разрешение и унификация с тех пор были включены во многие автоматизированные системы доказательства теорем и являются основой механизмов вывода, используемых в логическом программировании и языке программирования Пролог. [5]
Робинсон был редактором-основателем журнала Logic Programming и получил множество наград. К ним относятся стипендия Гуггенхайма в 1967 году , Американского математического общества в области автоматического доказательства теорем 1985 года, награда [6] стипендия AAAI 1990 г., [7] премия Эрбрана за выдающийся вклад в автоматическое мышление 1996 г., [8] [9] и «Основатель логического программирования» Ассоциации почетное звание логического программирования в 1997 году. [10] Он получил почетную докторскую степень Католического университета Левена в 1988 году. [11] Уппсальский университет , 1994 г., [12] и Политехнический университет Мадрида , 2003 г. [13] [14] Робинсон умер в Портленде, штат Мэн , 5 августа 2016 года от разрыва аневризмы после операции по поводу рака поджелудочной железы. [3]
В 1994 году он получил Премию старшего научного сотрудника Гумбольдта по просьбе Вольфганга Бибеля , которая включала шестимесячное пребывание на факультете компьютерных наук Технического университета Дармштадта . [15] [16]
Избранные публикации
[ редактировать ]- Робинсон, Дж. Алан; Воронков, Андрей , ред. (2001). Справочник по автоматизированному рассуждению . МТИ Пресс . ISBN 0-444-50813-9 .
- Габбай, Дов М .; Хоггер, Кристофер Джон; Робинсон, Дж. А., ред. (1993-1998). Справочник по логике в искусственном интеллекте и логическом программировании . Том. 1-5, Издательство Оксфордского университета.
- Арбиб, Майкл А .; Робинсон, Дж. Алан, ред. (1990). Естественные и искусственные параллельные вычисления . МТИ Пресс . ISBN 0-262-01120-4 .
- Робинсон, Дж. А. (1979). Логика: форма и функция . Издательство Эдинбургского университета . ISBN 0-85224-305-7 .
- Робинсон, Джон Алан (январь 1965 г.). «Машинно-ориентированная логика, основанная на принципе разрешения» . Дж. АКМ . 12 (1): 23–41. дои : 10.1145/321250.321253 . S2CID 14389185 .
- Робинсон, Джон Алан (1957). Причинность, вероятность и свидетельство (кандидатская диссертация). Принстонский университет. OCLC 83304635 .
См. также
[ редактировать ]- Резольвентный метод Робинсона - альтернатива алгоритму Куайна – МакКласки для минимизации булевых функций
Примечания
[ редактировать ]- ^ «Запись философского семейного древа» . Архивировано из оригинала 28 октября 2014 года . Проверено 13 сентября 2014 г.
- ↑ Резюме Джона Алана Робинсона , upm.es, дата доступа 12 августа 2016 г.
- ^ Jump up to: а б «Джон Алан Робинсон, Некролог» . Нью-Йорк Таймс . 17 августа 2016 г. Проверено 2 ноября 2019 г.
- ^ Почетный факультет инженерии и информатики Сиракузского университета, по состоянию на 2 ноября 2019 г.
- ^ Команда разработчиков Coq (18 октября 2018 г.). Справочное руководство Coq: версия 8.10+альфа (PDF) . п. 3. Архивировано из оригинала (PDF) 19 октября 2018 года . Проверено 19 октября 2018 г.
Автоматизированное доказательство теорем было впервые предложено в 1960-х годах Дэвисом и Патнэмом в исчислении высказываний. Полная механизация (в смысле процедуры полурешения) классической логики первого порядка была предложена в 1965 году Дж. А. Робинсоном с помощью единственного однородного правила вывода, называемого разрешением . Разрешение основано на решении уравнений в свободных алгебрах (т.е. термальных структурах) с использованием алгоритма объединения. Многие усовершенствования разрешения были изучены в 1970-х годах, но было реализовано лишь несколько убедительных реализаций, за исключением, конечно, PROLOG, в некотором смысле возникшего в результате этих усилий.
- ^ Призы AMS за автоматическое доказательство теорем
- ^ Список стипендиатов AAAI
- ^ «Премия Эрбрана 1996: Дж. Алан Робинсон» . Архивировано из оригинала 7 марта 2007 года . Проверено 13 января 2007 г.
- ^ «Премия CADE Herbrand» . Архивировано из оригинала 13 сентября 2014 года . Проверено 13 сентября 2014 г.
- ^ Награды ALP
- ^ Обзор почетных докторских степеней КУ Левена 1966–2012 гг.
- ^ «Почетный доктор – Уппсальский университет, Швеция» . 9 июня 2023 г.
- ^ Почетные докторские степени UP Madrid 1973–2013 гг.
- ↑ Почетная докторская степень UP Madrid Джона Алана Робинсона, 1 октября 2003 г.
- ^ «Профиль Джона Алана Робинсона в сети Гумбольдта» . www.humboldt-foundation.de . Проверено 2 ноября 2019 г. [ постоянная мертвая ссылка ]
- ^ Библия Леонхарда Вольфганга (2017), Размышления перед рефлексами - Мемуары исследователя (на немецком языке) (1-е изд.), Геттинген: Cuvillier Verlag, ISBN 9783736995246
Внешние ссылки
[ редактировать ]- Джон Алан Робинсон на DBLP библиографическом сервере
- Книги, перечисленные MIT Press
- 1930 рождений
- смертей в 2016 г.
- Британские ученые-компьютерщики
- Американские ученые-компьютерщики
- Британские математики XX века
- Британские математики XXI века
- Американские математики XX века
- Американские математики XXI века
- Выпускники Университета Орегона
- Выпускники Принстонского университета
- Преподаватели Университета Райса
- Преподаватели Сиракузского университета
- Формальные методы люди
- Британские эмигранты в США
- Члены Ассоциации развития искусственного интеллекта
- Редакторы американских академических журналов
- Выпускники Кембриджского университета
- Математики из Нью-Йорка (штат)