Ричард Уолдингер
Ричард Уолдингер | |
|---|---|
| Национальность | Американский |
| Альма-матер | Университет Карнеги Меллон |
| Научная карьера | |
| Учреждения | НИИ Международный |
| Докторантура | Герберт А. Саймон [1] |
Ричард Джей Уолдингер — исследователь компьютерных наук в International SRI Центре искусственного интеллекта (где он работает с 1969 года), чьи интересы сосредоточены на применении автоматизированных дедуктивных рассуждений для решения проблем разработки программного обеспечения и искусственного интеллекта .
Молодость образование и
В своей диссертации ( Университет Карнеги-Меллон , 1969), посвященной извлечению компьютерных программ из доказательств теорем, он обнаружил, что применение правила разрешения объясняет появление условного перехода в извлеченной программе, в то время как использование Принцип математической индукции привел к появлению рекурсии и других повторяющихся конструкций. [2]
Карьера [ править ]
Уолдингер начал работать в SRI International, тогда известном как Стэнфордский исследовательский институт, в 1969 году и остается там с тех пор. С 1970 года он подает кофе и печенье в своем офисе в SRI два раза в неделю. [3] [4]
QA4 [ править ]
Уолдингер сотрудничал с Корделлом Грином , Робертом Йейтсом, Джеффом Рулифсоном и Яном Дерксеном над QA4 , языком искусственного интеллекта, похожим на PLANNER , предназначенным для автоматического планирования и доказательства теорем. [5] В QA4 было введено понятие контекста, а также ассоциативно-коммутативной унификации, что сделало ассоциативные и коммутативные аксиомы для операторов не только ненужными, но и невыразимыми. Они применили этот язык при планировании робота SRI Шейки . Вместе с Берни Элспасом и Карлом Левиттом Уолдингер использовал QA4 для проверки программы (доказывая, что программа делает то, что должна), получая автоматические проверки для алгоритма унификации и программы Хоара FIND.
Синтез программы [ править ]
В то время как диссертация Уолдингера касалась синтеза аппликативных программ, которые возвращают результат, но не производят побочных эффектов, затем Уолдингер обратился к синтезу императивных программ, которые выполняют и то, и другое. [6] Чтобы разобраться с проблемой одновременного достижения целей, которые мешают друг другу, он ввел понятие регрессии цели, которое было получено из более ранних работ по верификации программ Флойда , Кинга, Хоара и Дейкстры . Поскольку императивные программы аналогичны планам, этот подход применим и к классическим задачам планирования ИИ.
В сотрудничестве с Зохаром Манной из Стэнфордского университета Уолдингер разработал неклаузальное разрешение — форму разрешения, которая не требует перевода логических предложений в ограниченную клаузальную форму. Перевод не только был дорогим, но и иногда патологически усложнял доказательство полученной теоремы; эти проблемы были решены новым правилом. Они применили правило на бумаге, чтобы произвести подробный синтез алгоритма объединения. В отдельной статье они синтезировали новый алгоритм извлечения квадратного корня; они обнаружили, что понятие двоичного поиска возникает спонтанно при однократном применении правила разрешения к определению квадратного корня. [7] [8]
СНАРК [ править ]
Некоторые из идей Манны и Уолдингера по доказательству теорем были включены в конструкцию средства доказательства теорем SNARK Марка Стикеля . Исследователи НАСА под руководством Майка Лоури использовали SNARK при реализации среды разработки программного обеспечения Amphion, которая использовалась для создания программ анализа данных миссий НАСА для планетарных астрономов. Программное обеспечение, автоматически созданное Amphion, использовалось для планирования фотографий миссии НАСА «Кассини-Гюйгенс» ; на сегодняшний день это, пожалуй, наиболее практичное применение программного обеспечения, автоматически созданного дедуктивными методами.
Система SNARK была включена Институтом Кестрел в их среду разработки программного обеспечения Specware, которая использовалась Уолдингером для проверки аксиоматизации первого порядка DAML , языка разметки агента DARPA , и его преемника OWL . СНАРК обнаружил несоответствия не только в аксиомах DAML, но и в аксиомах основополагающего языка KIF , на котором была основана аксиоматизация DAML. Недавно Уолдингер работал над применением дедуктивных методов для ответа на вопросы по географии, биологии и анализу интеллекта. В сотрудничестве с Институтом Кестрел он использовал SNARK для аутентификации протоколов безопасности.
и награды Членство
В 1991 году Уолдингер был избран членом Ассоциации по развитию искусственного интеллекта . [9]
Личная жизнь [ править ]
В личной жизни Уолдингер занимается айкидо, йогой и медитацией. Член авторитетной писательской группы, он публикует кулинарную журналистику и эротическую фантастику. [10] Он женат, имеет двоих детей и троих внуков.
Ссылки [ править ]
- ^ «Ричард Джей Уолдингер» . Проект ИИ-генеалогии . Проверено 15 марта 2012 г.
- ^ Уолдингер, Ричард Дж (1969). Автоматическое построение программ с использованием доказательства теорем (Диссертация). Университета Карнеги-Меллона Факультет компьютерных наук .
- ^ «Кофе и печенье Ричарда Уолдингера» . Центр искусственного интеллекта . Проверено 15 марта 2012 г.
- ^ Нильс Дж. Нильссон (1984). «Введение в издание COMTEX на микрофишах технических заметок НИИ Центра искусственного интеллекта» . Журнал ИИ . Том. 5, нет. 1. п. 46.
- ^ Джефф Рулифсон ; Ян Дерксен; Ричард Уолдингер (ноябрь 1973 г.). «QA4, процедурное исчисление для интуитивного мышления». Техническая записка 73 НИИ ИИ Центра .
- ^ Зоар Манна ; Ричард Уолдингер (1978). «Иногда ли «когда-нибудь» лучше, чем «всегда»? (Периодические утверждения при доказательстве корректности программы)» . Коммуникации АКМ . 21 (2): 159–172. дои : 10.1145/359340.359353 . S2CID 5905332 .
- ^ Манна, Зоар; Ричард Уолдингер (1987). «Дедуктивный синтез императивных программ LISP». АААИ : 155–160.
- ^ Манна, Зоар; Ричард Уолдингер (1993). Дедуктивные основы компьютерного программирования . Аддисон-Уэсли.
- ^ «Избранные члены AAAI» . Ассоциация по развитию искусственного интеллекта . Проверено 15 марта 2012 г.
- ^ "Авторы" . Истории на одной странице . Проверено 15 марта 2012 г.
Дальнейшее чтение [ править ]
- Герд Гроссе и Рихард Вальдингер. «К теории одновременных действий» EWSP 1991: 78-87.
- Зоар Манна и Ричард Уолдингер. «Происхождение парадигмы бинарного поиска» Sci. Вычислить. Программа. 9(1): 37-83 (1987)
Внешние ссылки [ править ]
| Международный | |
|---|---|
| академики | |
