Джон Алан Робинсон (9 марта 1930 – 5 августа 2016) был философом, математиком и ученым-компьютерщиком . Он был почетным профессором Сиракузского университета .
Главный вклад Алана Робинсона — в основы автоматизированного доказательства теорем . Его алгоритм объединения устранил один из источников комбинаторного взрыва в программах доказательства резолюций ; он также подготовил почву для парадигмы логического программирования , в частности для языка Пролог . Робинсон получил премию Эрбрана 1996 года за выдающийся вклад в автоматизированное рассуждение .
Робинсон родился в Галифаксе , Йоркшир, Англия, в 1930 году [2] и уехал в Соединенные Штаты в 1952 году, получив степень по классике в Кембриджском университете . Он изучал философию в Университете Орегона , а затем перешел в Принстонский университет , где в 1956 году получил степень доктора философии. Затем он работал в DuPont аналитиком по исследованию операций , где изучал компьютерное программирование и самостоятельно изучал математику . В 1961 году он перешел в Университет Райса , проводя лето в качестве приглашенного исследователя в Отделе прикладной математики Аргоннской национальной лаборатории . В 1967 году он перешел в Сиракузский университет в качестве почетного профессора логики и компьютерных наук [3] и стал почетным профессором в 1993 году. [4]
Именно в Аргонне Робинсон заинтересовался автоматизированным доказательством теорем и разработал унификацию и принцип разрешения. С тех пор резолюция и унификация были включены во многие автоматизированные системы доказательства теорем и являются основой для механизмов вывода, используемых в логическом программировании и языке программирования Пролог. [5]
Робинсон был основателем и главным редактором журнала « Журнал логического программирования» и получил множество наград. К ним относятся стипендия Гуггенхайма в 1967 году , премия Американского математического общества Milestone Award в области автоматического доказательства теорем 1985 года [6], стипендия AAAI 1990 года [7], премия Эрбрана за выдающийся вклад в автоматическое рассуждение 1996 года [8] [9] и почетное звание Ассоциации логического программирования «Основатель логического программирования» в 1997 году. [10] Он получил почетные докторские степени от Католического университета Лёвена в 1988 году [11] Университета Уппсалы в 1994 году [12] и Мадридского политехнического университета в 2003 году [13] [14] Робинсон умер в Портленде, штат Мэн, 5 августа 2016 года от разрыва аневризмы после операции по поводу рака поджелудочной железы. [3]
В 1994 году по просьбе Вольфганга Бибеля он получил премию имени Гумбольдта для старших научных сотрудников , которая включала шестимесячное пребывание на кафедре компьютерных наук Дармштадтского технического университета . [15] [16]
Автоматизированное доказательство теорем было впервые применено в 1960-х годах Дэвисом и Патнэмом в исчислении высказываний. Полная механизация (в смысле процедуры полурешения) классической логики первого порядка была предложена в 1965 году JA Robinson с единственным единым правилом вывода, называемым
резолюцией
. Резолюция основана на решении уравнений в свободных алгебрах (т. е. структурах терминов) с использованием алгоритма унификации. В 1970-х годах было изучено множество уточнений резолюции, но было реализовано несколько убедительных реализаций, за исключением, конечно, того, что PROLOG в некотором смысле возник из этих усилий.