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

Ричард Джей Waldinger является компьютерными науками исследователь SRI International «s искусственного интеллекта Центр (где он работал с 1969 года) , чьи интересы сосредоточены на применении автоматизированной дедукции к проблемам в программной инженерии и искусственном интеллекте .

Ранняя жизнь и образование [ править ]

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

Карьера [ править ]

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

QA4 [ править ]

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

Синтез программы [ править ]

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

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

СНАРК [ править ]

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

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

Членство и награды [ править ]

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

Личная жизнь [ править ]

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

Ссылки [ править ]

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

Дальнейшее чтение [ править ]

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

Внешние ссылки [ править ]

  • Домашняя страница Ричарда Уолдингера