Джон Алан Робинсон (9 марта 1930 — 5 августа 2016) был философом, математиком и ученым-компьютерщиком . Он был почетным профессором Сиракузского университета .
Основной вклад Алана Робинсона заключается в создании основ автоматизированного доказательства теорем . Его алгоритм унификации устранил один источник комбинаторного взрыва в пруверах разрешения ; он также подготовил почву для парадигмы логического программирования , в частности для языка Пролог . Робинсон получил в 1996 году премию Хербранда за выдающийся вклад в автоматизированное мышление .
Робинсон родился в Галифаксе , Йоркшир, Англия, в 1930 году [2] и уехал в Соединенные Штаты в 1952 году, получив степень классика в Кембриджском университете . Он изучал философию в Орегонском университете, а затем перешел в Принстонский университет , где в 1956 году получил докторскую степень по философии. Затем он работал в Du Pont в качестве аналитика по исследованию операций , где он изучил программирование и самостоятельно изучил математику . Он переехал в Университет Райса в 1961 году, проводя лето в качестве приглашенного исследователя в Аргоннской национальной лаборатории .Отдел прикладной математики. Он перешел в Сиракузский университет в качестве заслуженного профессора логики и компьютерных наук в 1967 году [3] и стал почетным профессором в 1993 году [4] .
Именно в Аргонне Робинсон заинтересовался автоматизированным доказательством теорем и разработал принцип унификации и разрешения. С тех пор разрешение и унификация были включены во многие автоматизированные системы доказательства теорем и являются основой для механизмов вывода, используемых в логическом программировании и языке программирования Prolog. [5]
Робинсон был редактором-основателем журнала Logic Programming и получил множество наград. К ним относятся стипендия Гуггенхайма в 1967 г., премия Американского математического общества за веху в области автоматического доказательства теорем 1985 г. [6] , стипендия AAAI в 1990 г., [7] премия Хербранда за выдающийся вклад в автоматическое рассуждение 1996 г., [8] [9] и Почетное звание Ассоциации логического программирования « Основатель логического программирования» в 1997 году . Уппсальский университет , 1994 г., [12] и Мадридский политехнический университет , 2003 г. [13] [14] Робинсон умер в Портленде, штат Мэн, 5 августа 2016 г. от разрыва аневризмы после операции по поводу рака поджелудочной железы. [3]
В 1994 году он получил премию Humboldt Senior Scientist Award по просьбе Вольфганга Бибеля , которая включала шестимесячное пребывание на факультете компьютерных наук Технического университета Дармштадта . [15] [16]