Jump to content

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

(Перенаправлено с Дж. А. Робинсона )

Джон Алан Робинсон
Робинсон в 2012 году
Рожденный ( 1930-03-09 ) 9 марта 1930 г.
Умер 5 августа 2016 г. (05.08.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]

Избранные публикации

[ редактировать ]

См. также

[ редактировать ]

Примечания

[ редактировать ]
  1. ^ «Запись философского семейного древа» . Архивировано из оригинала 28 октября 2014 года . Проверено 13 сентября 2014 г.
  2. Резюме Джона Алана Робинсона , upm.es, дата доступа 12 августа 2016 г.
  3. ^ Jump up to: а б «Джон Алан Робинсон, Некролог» . Нью-Йорк Таймс . 17 августа 2016 г. Проверено 2 ноября 2019 г.
  4. ^ Почетный факультет инженерии и информатики Сиракузского университета, по состоянию на 2 ноября 2019 г.
  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
[ редактировать ]
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: df1d1920db9af2b605542d81372db196__1713001080
URL1:https://arc.ask3.ru/arc/aa/df/96/df1d1920db9af2b605542d81372db196.html
Заголовок, (Title) документа по адресу, URL1:
John Alan Robinson - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)