Джон Алан Робинсон | |
---|---|
Джон Алан Робинсон в 2012 году | |
Родился | (1930-03- 09) 9 марта 1930. Галифакс, Западный Йоркшир, Великобритания |
Умер | 5 августа 2016 (2016-08-05) (86 лет). Портленд, Мэн, США |
Alma mater | Кембриджский университет. Университет Орегона. Принстонский университет |
Известный | принцип разрешения, унификация |
Награды | AMS Milestone Award 1985, премия Humboldt Senior Scientist 1995, Herbrand Award 1996 |
Научная карьера | |
Учреждения | Сиракузский университет |
Диссертация | Причинно-следственная связь, вероятность и свидетельство (1957) |
Докторант | Карл Хемпель |
Джон Алан Робинсон (9 марта 1930 - 5 августа 2016) был философом, математиком и ученым-компьютерщиком. Он был почетным профессором в Сиракузском университете.
. Главный вклад Алана Робинсона - создание автоматизированного доказательства теорем. Его алгоритм унификации устранил один источник комбинаторного взрыва в пруверах ; он также подготовил почву для парадигмы логического программирования, в частности для языка Prolog. Робинсон получил в 1996 г. Премию Хербранда за выдающийся вклад в автоматизированное мышление.
Робинсон родился в Галифаксе, Йоркшир, Англия в 1930 году и уехал в Соединенные Штаты в 1952 году со степенью классика от Кембриджский университет. Он изучал философию в Университете штата Орегон, а затем перешел в Принстонский университет, где в 1956 году получил докторскую степень по философии. Затем он работал в Du Pont в качестве исследования операций аналитик, где он изучил программирование и сам выучил математику. Он переехал в Университет Райса в 1961 году, проводя лето в качестве приглашенного исследователя в отделе прикладной математики Аргоннской национальной лаборатории. Он перешел в Сиракузский университет в качестве заслуженного профессора логики и информатики в 1967 году и стал почетным профессором в 1993 году.
Именно в Аргонне Робинсон заинтересовался автоматическим доказательством теорем и разработал унификацию и принцип разрешения. С тех пор разрешение и унификация были включены во многие автоматизированные системы доказательства теорем и являются основой механизмов вывода, используемых в логическом программировании и языке программирования Prolog.
Робинсон был редактором-основателем журнала Journal of Logic Programming и получил множество наград. К ним относятся стипендия Гуггенхайма в 1967 г., награда Американского математического общества Milestone Award в области автоматического доказательства теорем 1985 г., стипендия AAAI 1990 г., премия Хербранда за выдающийся вклад в Автоматическое рассуждение в 1996 году и почетное звание Ассоциации логического программирования Основатель логического программирования в 1997 году. Он получил почетные докторские степени от Католикского университета Лёвена 1988, Уппсальский университет 1994 и Политехнический университет Мадрида 2003. Робинсон умер в Портленде, штат Мэн 5 августа 2016 года от разрыва аневризмы после операции по поводу рака поджелудочной железы.
В 1994 году он получил Премию старшего ученого Гумбольдта в запрос Вольфганга Бибеля, который включал шестимесячное пребывание на факультете компьютерных наук Технического университета Дармштадта.