Ричард Уолдингер - Richard Waldinger

Ричард Уолдингер
НациональностьАмериканец
Альма-матерУниверситет Карнеги Меллон
Научная карьера
УчрежденияSRI International
ДокторантГерберт А. Саймон[1]

Ричард Джей Уолдингер исследователь информатики в SRI International с Центр Искусственного Интеллекта (где он работал с 1969 г.), интересы которого сосредоточены на применении автоматизированных дедуктивное мышление к проблемам в программная инженерия и искусственный интеллект.

ранняя жизнь и образование

В его диссертации (Университет Карнеги Меллон, 1969), который касался извлечения компьютерных программ из доказательств теорем, он обнаружил, что применение правила разрешения объясняет появление условной ветви в извлеченной программе, в то время как использование принципа математической индукции привело к введению рекурсия и другие повторяющиеся конструкции.[2]

Карьера

Вальдингер начал свою деятельность в SRI International, тогда известном как Стэнфордский исследовательский институт, в 1969 году и с тех пор остается там. С 1970 года он подает кофе и печенье в своем офисе в SRI два раза в неделю.[3][4]

QA4

Уолдингер сотрудничал с Корделлом Грином, Робертом Йейтсом, Джеффом Рулифсоном и Яном Дерксеном на QA4, а ПЛАНИРОВЩИК -подобный язык искусственного интеллекта, предназначенный для автоматического планирования и доказательства теорем.[5] QA4 ввел понятие контекста, а также ассоциативно-коммутативного объединения, которое сделало ассоциативные и коммутативные аксиомы для операторов не только ненужными, но и невыразимыми. Они применили этот язык к планированию робота SRI, Shakey. Вместе с Берни Эльспасом и Карлом Левиттом Вальдингер использовал QA4 для проверки программы (доказательства того, что программа делает то, что она должна делать), получения автоматических проверок для алгоритма унификации и Hoare программа НАЙТИ.

Программный синтез

В то время как тезис Уолдингера касался синтеза прикладных программ, которые возвращают результат, но не вызывают побочных эффектов, Вальдингер затем обратился к синтезу императивных программ, которые делают и то, и другое.[6] Чтобы решить проблему одновременного достижения целей, которые мешают друг другу, он ввел понятие регрессии целей, которое было получено в результате более ранней работы по верификации программ Флойд, Король, Hoare, и Dijkstra. Поскольку императивные программы аналогичны планам, этот подход был применим и к классическим задачам планирования ИИ.

В сотрудничестве с Зохар Манна, из Стэндфордский Университет Вальдингер разработал неклаузальную резолюцию, форму разрешения, которая не требовала перевода логических предложений в ограниченную клаузальную форму. Мало того, что перевод был дорогостоящим, но также иногда патологически усложнял доказательство получившейся теоремы; эти проблемы были обойдены новым правилом. Они применили правило на бумаге, чтобы произвести подробный синтез алгоритма унификации. В отдельной статье они синтезировали новый алгоритм извлечения квадратного корня; они обнаружили, что понятие двоичного поиска появляется спонтанно при однократном применении правила разрешения к определению квадратного корня.[7][8]

СНАРК

Некоторые идеи Манна и доказательства теорем Уолдингера были включены в проект Марка Стикеля. Средство доказательства теорем SNARK. НАСА Исследователи под руководством Майка Лоури использовали SNARK при реализации среды разработки программного обеспечения Amphion, которая использовалась для создания программ для анализа данных миссий НАСА для планетарных астрономов. Программное обеспечение, автоматически созданное Amphion, использовалось для планирования фотосъемки для Кассини-Гюйгенс Миссия НАСА; на сегодняшний день это, пожалуй, наиболее практичное приложение программного обеспечения, созданного автоматически дедуктивными методами.

Система SNARK была включена Институт пустельги в их среду разработки программного обеспечения Specware, которую Вальдингер использовал для проверки аксиоматизации первого порядка DAML, то DARPA язык разметки агента и его преемник, СОВА. SNARK обнаружил несоответствия не только в аксиомах DAML, но и в аксиомах основополагающего языка. КИФ, на котором основана аксиоматизация DAML. В последнее время Вальдингер работал над применением дедуктивных методов для ответа на вопросы по географии, биологии и анализу интеллекта. В сотрудничестве с Институтом Kestrel он использовал SNARK для аутентификации протоколов безопасности.

Членство и награды

В 1991 году Вальдингер был избран членом Ассоциация развития искусственного интеллекта.[9]

Личная жизнь

В личной жизни Вальдингер изучает айкидо, йогу и медитацию. Член авторитетной писательской группы, он публиковал статьи о кулинарии и эротической литературе.[10]Женат, имеет двоих детей и троих внуков.

Рекомендации

  1. ^ "Ричард Джей Уолдингер". Проект AI Genealogy. Получено 2012-03-15.
  2. ^ Уолдингер, Ричард Дж (1969). Автоматическое построение программ с использованием доказательства теорем (Тезис). Университет Карнеги Меллон Департамент компьютерных наук.
  3. ^ "Кофе и печенье Ричарда Уолдингера". Центр Искусственного Интеллекта. Получено 2012-03-15.
  4. ^ Нильс Дж. Нильссон (1984). «Знакомство с изданием COMTEX Microfiche Edition Технических заметок SRI Центра искусственного интеллекта». Журнал AI. 5 (1). п. 46.
  5. ^ Джефф Рулифсон; Ян Дерксен; Ричард Уолдингер (ноябрь 1973 г.). "QA4, процедурное исчисление для интуитивного мышления". Техническая записка 73 SRI AI Center.
  6. ^ Зохар Манна; Ричард Уолдингер (1978). «Иногда» лучше, чем «всегда»? (Периодические утверждения в доказательстве правильности программы) ». Коммуникации ACM. 21 (2): 159–172. Дои:10.1145/359340.359353.
  7. ^ Манна, Зоар; Ричард Уолдингер (1987). "Дедуктивный синтез императивных программ LISP". AAAI: 155–160.
  8. ^ Манна, Зоар; Ричард Уолдингер (1993). Дедуктивные основы компьютерного программирования. Эддисон-Уэсли.
  9. ^ «Избранные стипендиаты AAAI». Ассоциация развития искусственного интеллекта. Получено 2012-03-15.
  10. ^ "Авторы". Истории на одной странице. Получено 2012-03-15.

дальнейшее чтение

  • Герд Гроссе и Ричард Вальдингер. «К теории одновременных действий» EWSP 1991: 78-87.
  • Зохар Манна и Ричард Уолдингер. "Происхождение парадигмы двоичного поиска" Sci. Comput. Программа. 9 (1): 37-83 (1987).

внешняя ссылка