Войти
| Ричард Уолдингер | |
|---|---|
| Национальность | Американец |
| Альма-матер | Университет Карнеги Меллон |
| Научная карьера | |
| Учреждения | SRI International |
| Докторант | Герберт А. Саймон |
Ричард Джей Waldinger является компьютерными науками исследователь SRI International «s искусственного интеллекта Центр (где он работал с 1969 года), чьи интересы сосредоточены на применении автоматизированной дедукции к проблемам в программной инженерии и искусственном интеллекте.
В своей диссертации ( Университет Карнеги-Меллона, 1969), которая касалась извлечения компьютерных программ из доказательств теорем, он обнаружил, что применение правила разрешения объясняет появление условной ветви в извлеченной программе, в то время как использование Принцип математической индукции вызвал введение рекурсии и других повторяющихся конструкций.
Вальдингер начал свою деятельность в SRI International, тогда известном как Стэнфордский исследовательский институт, в 1969 году и с тех пор остается там. С 1970 года он подает кофе и печенье в своем офисе в SRI два раза в неделю.
Waldinger сотрудничал с Корделл Грин, Роберт Йейтс, Джефф Рулифсон и Ян Derksen на QA4, в PLANNER -like искусственного языка интеллекта, ориентированных на автоматическое планирование и доказательства теорем. QA4 ввел понятие контекста, а также ассоциативно-коммутативного объединения, которое сделало ассоциативные и коммутативные аксиомы для операторов не только ненужными, но и невыразимыми. Они применили этот язык при планировании робота SRI Shakey. Вместе с Берни Эльспасом и Карлом Левиттом Уолдингер использовал QA4 для проверки программы (доказывая, что программа делает то, что она должна делать), получая автоматические проверки для алгоритма унификации и программы FIND Хоара.
В то время как тезис Уолдингера касался синтеза прикладных программ, которые возвращают результат, но не вызывают побочных эффектов, Вальдингер затем обратился к синтезу императивных программ, которые делают и то, и другое. Чтобы решить проблему одновременного достижения целей, которые мешают друг другу, он ввел понятие регрессии целей, которое было получено из более ранней работы Флойда, Кинга, Хора и Дейкстры по верификации программ. Поскольку императивные программы аналогичны планам, этот подход был применим и к классическим задачам планирования ИИ.
В сотрудничестве с Зохаром Манной из Стэнфордского университета Вальдингер разработал решение без декларации, форму разрешения, которая не требовала перевода логических предложений в ограниченную клаузальную форму. Мало того, что перевод был дорогостоящим, но также иногда патологически усложнял доказательство получившейся теоремы; эти проблемы были обойдены новым правилом. Они применили правило на бумаге, чтобы произвести подробный синтез алгоритма унификации. В отдельной статье они синтезировали новый алгоритм извлечения квадратного корня; они обнаружили, что понятие двоичного поиска возникает спонтанно при однократном применении правила разрешения к определению квадратного корня.
Некоторые идеи Манна и Уолдингера в доказательстве теорем были включены в конструкцию средства доказательства теорем SNARK Марка Стикеля. Исследователи НАСА во главе с Майком Лоури использовали SNARK при реализации среды разработки программного обеспечения Amphion, которая использовалась для создания программ для анализа данных миссий НАСА для планетных астрономов. Программное обеспечение, автоматически созданное Amphion, использовалось для планирования фотосъемки для миссии НАСА « Кассини-Гюйгенс »; на сегодняшний день это, пожалуй, наиболее практичное приложение программного обеспечения, созданного автоматически дедуктивными методами.
Система SNARK была включена Институтом Kestrel в их среду разработки программного обеспечения Specware, которая использовалась Уолдингером для проверки аксиоматизации первого порядка DAML, языка разметки агента DARPA и его преемника, OWL. SNARK обнаружил несоответствия не только в аксиомах для DAML, но и в аксиомах для базового языка KIF, на котором базируется аксиоматизация DAML. В последнее время Вальдингер работал над применением дедуктивных методов для ответа на вопросы по географии, биологии и анализу интеллекта. В сотрудничестве с Институтом Kestrel он использовал SNARK для аутентификации протоколов безопасности.
В 1991 году Уолдингер был избран членом Ассоциации по развитию искусственного интеллекта.
В личной жизни Вальдингер изучает айкидо, йогу и медитацию. Член авторитетной писательской группы, он публикует статьи о кулинарии и эротической литературе. Женат, имеет двоих детей и троих внуков.
