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

Джон Алан Робинсон (англ. John Alan Robinson; 9 марта 1930, Халл, Англия — 5 августа 2016, Портленд, штат Мэн, США) — британский и американский математик, философ и логик, известный прежде всего как создатель метода резолюций — фундаментального алгоритма автоматического доказательства теорем в логике первого порядка. Внёс крупный вклад в развитие искусственного интеллекта, вычислительной логики и математического обеспечения компьютеров.

Биография

Ранние годы и образование

Джон Алан Робинсон родился 9 марта 1930 года в городе Халл (Йоркшир, Англия). Его отец был юристом, мать — учительницей. В 1948 году поступил в Кембриджский университет (Колледж Святого Иоанна), где изучал математику и философию. В 1952 году получил степень бакалавра с отличием по математике и философии.

Академическая карьера

В 1953 году переехал в США, где поступил в аспирантуру Принстонского университета. В 1956 году защитил диссертацию по математической логике под руководством Алонзо Чёрча. После защиты работал в Корнеллском университете (1956–1960), затем в Университете Райса (1960–1963). В 1963 году стал профессором математики и компьютерных наук в Сиракузском университете (штат Нью-Йорк), где проработал до выхода на пенсию в 1994 году.

Смерть

Джон Алан Робинсон умер 5 августа 2016 года в Портленде (штат Мэн) в возрасте 86 лет.

Научные достижения

Метод резолюций (1965)

Главное открытие Робинсона — метод резолюций, опубликованный в 1965 году в статье «A Machine-Oriented Logic Based on the Resolution Principle» («Машино-ориентированная логика, основанная на принципе резолюции»). Метод резолюций представляет собой полный алгоритм доказательства теорем в логике первого порядка, использующий принцип опровержения: для доказательства формулы строится её отрицание, затем доказывается, что множество дизъюнктов, образованных из этого отрицания, является невыполнимым. Ключевая идея — применение правила резолюции, которое позволяет из двух дизъюнктов (логических формул вида «A1 или A2 или … или An») выводить новый дизъюнкт, если одна из частей первого дизъюнкта является отрицанием одной из частей второго.

Метод резолюций стал основой для систем автоматического доказательства теорем, таких как Prolog, Otter, E, и широко используется в искусственном интеллекте, верификации программ, криптографии и других областях.

Унификация

Робинсон также разработал алгоритм унификации — процедуру нахождения наиболее общего подстановчика, который делает два терма или литерала тождественными. Унификация является критическим компонентом метода резолюций и используется во многих системах логического программирования и обработки естественного языка.

Другие работы

Робинсон занимался также вопросами логики с модальностями, неклассической логики и оснований математики. В 1990-х годах работал над проблемой автоматического доказательства теорем в неклассических логиках.

Влияние и признание

Научное сообщество

Метод резолюций признан одним из важнейших достижений в области логического программирования и искусственного интеллекта. Он заложил основы для развития языков логического программирования, таких как Prolog (1972), и для многих систем автоматического доказательства теорем.

Номинации и премии

• 1996 год — Медаль Хербранда — наибольшая ежегодная награда в области автоматического доказательства теорем (названа в честь Жака Хербранда).
• 2005 год — избран членом Ассоциации вычислительной техники (ACM Fellow).
• 2011 год — почётный доктор Университета Льежа (Бельгия).

Основные публикации

Ключевые статьи

1. Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1), 23–41.
2. Robinson, J. A. (1979). Logic: Form and Function. North-Holland.

Книги

• Logic: Form and Function (1979) — учебное пособие по математической логике, ориентированное на применение в информатике.
• The Nature of Logic (1991) — сборник статей по основаниям логики.

Интересные факты

1. Происхождение термина «метод резолюций»: Робинсон выбрал слово «резолюция» от лат. resolutio — «разложение, растворение», подчёркивая, что доказательство сводится к разложению логической формулы на более простые части.
2. Влияние на Prolog: Метод резолюций лёг в основу языка Prolog, созданного Робертом Кули и Аленом Колмероэ в 1972 году. Prolog стал одним из первых декларативных языков программирования.
3. Отказ от дальнейшего развития: В 1970-х годах Робинсон отошёл от активной разработки алгоритмов автоматического доказательства теорем, сосредоточившись на философских вопросах логики.

Критика и ограничения метода резолюций

Несмотря на фундаментальную важность, метод резолюций имеет ограничения:

• Экспоненциальная сложность: В худшем случае количество шагов доказательства может расти экспоненциально относительно размера входных данных.
• Необходимость эвристик: Для практического применения требуется тщательная оптимизация (стратегии упорядочения, отсечения, семантические фильтры).
• Не применим к некоторым логикам: Метод резолюций работает только для логики первого порядка и не обобщается напрямую на логики более высоких порядков или модальные логики без дополнительных модификаций.

Тем не менее, усовершенствованные версии метода (в частности, с использованием стратегии линейной резолюции и семантических ограничений) до сих пор остаются одними из наиболее эффективных методов автоматического доказательства теорем в практических задачах.

Источники

1. Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1), 23–41.
2. Robinson, J. A. (1979). Logic: Form and Function. North-Holland.
3. Loveland, D. W. (1978). Automated Theorem Proving: A Logical Basis. North-Holland.
4. Chang, C. L., & Lee, R. C. T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press.
5. Некролог Джона Алана Робинсона, The New York Times, 12 августа 2016.