Джон Алан Робинсон

Джон Алан Робинсон
Джон Алан Робинсон
	Робинсон в 2012 году
Рожденный	9 марта 1930 г. ; Галифакс, Западный Йоркшир , Великобритания
Умер	5 августа 2016 г. (86 лет) ; Портленд, Мэн , США
Альма-матер	Кембриджский университет ; Университет Орегона ; Принстонский университет
Известный	принцип разрешения , унификация
Награды	Премия AMS Milestone 1985 г., премия старшего ученого Гумбольдта 1995 г., премия Эрбрана 1996 г.
	Научная карьера
Учреждения	Сиракузский университет
Диссертация	Причинность, вероятность и показания (1957)
Докторантура	Карл Хемпель

Джон Алан Робинсон (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 .

См. также

Резольвентный метод Робинсона [ de ] - альтернатива алгоритму Куайна – МакКласки для минимизации булевых функций

Примечания

^ «Запись философского семейного древа» . Архивировано из оригинала 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

[1] «Запись философского семейного древа» . Архивировано из оригинала 28 октября 2014 года . Проверено 13 сентября 2014 г.

[2] Резюме Джона Алана Робинсона , upm.es, дата доступа 12 августа 2016 г.

[nyt20160817-3] Jump up to: ^а ^б «Джон Алан Робинсон, Некролог» . Нью-Йорк Таймс . 17 августа 2016 г. Проверено 2 ноября 2019 г.

[4] Почетный факультет инженерии и информатики Сиракузского университета, по состоянию на 2 ноября 2019 г.

[coq-refman-5] Команда разработчиков Coq (18 октября 2018 г.). Справочное руководство Coq: версия 8.10+альфа (PDF) . п. 3. Архивировано из оригинала (PDF) 19 октября 2018 года . Проверено 19 октября 2018 г. Автоматизированное доказательство теорем было впервые предложено в 1960-х годах Дэвисом и Патнэмом в исчислении высказываний. Полная механизация (в смысле процедуры полурешения) классической логики первого порядка была предложена в 1965 году Дж. А. Робинсоном с помощью единственного однородного правила вывода, называемого разрешением . Разрешение основано на решении уравнений в свободных алгебрах (т.е. термальных структурах) с использованием алгоритма объединения. Многие усовершенствования разрешения были изучены в 1970-х годах, но было реализовано лишь несколько убедительных реализаций, за исключением, конечно, PROLOG, в некотором смысле возникшего в результате этих усилий.

[6] Призы AMS за автоматическое доказательство теорем

[7] Список стипендиатов AAAI

[8] «Премия Эрбрана 1996: Дж. Алан Робинсон» . Архивировано из оригинала 7 марта 2007 года . Проверено 13 января 2007 г.

[9] «Премия CADE Herbrand» . Архивировано из оригинала 13 сентября 2014 года . Проверено 13 сентября 2014 г.

[10] Награды ALP

[11] Обзор почетных докторских степеней КУ Левена 1966–2012 гг.

[12] «Почетный доктор – Уппсальский университет, Швеция» . 9 июня 2023 г.

[13] Почетные докторские степени UP Madrid 1973–2013 гг.

[14] Почетная докторская степень UP Madrid Джона Алана Робинсона, 1 октября 2003 г.

[15] «Профиль Джона Алана Робинсона в сети Гумбольдта» . www.humboldt-foundation.de . Проверено 2 ноября 2019 г. ^{[ постоянная мертвая ссылка ]}

[16] Библия Леонхарда Вольфганга (2017), Размышления перед рефлексами - Мемуары исследователя (на немецком языке) (1-е изд.), Геттинген: Cuvillier Verlag, ISBN 9783736995246

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

Базы данных авторитетного контроля
Международный	БЫСТРЫЙ ЯВЛЯЮТСЯ 2 ВИАФ
Национальный	Норвегия Франция 2 Данные БнФ 2 Германия Италия Израиль Бельгия Соединенные Штаты Латвия Хорватия Нидерланды
академики	Ассоциация вычислительной техники ЦиНии ДБЛП MathSciNet zbMATH
Другой	ИдРеф