リチャード・ウォルディンガー

リチャード・ジェイ・ウォルディンガーは、SRIインターナショナルの人工知能センター（1969年から勤務）のコンピュータサイエンス研究者であり、ソフトウェアエンジニアリングと人工知能の問題への自動演繹推論の応用に関心を持っています。

定理の証明からコンピュータプログラムを抽出することに関する彼の論文（カーネギーメロン大学、1969年）では、解決規則の適用により抽出されたプログラムに条件分岐が出現し、数学的帰納原理の使用により再帰やその他の反復構造が導入されることを発見しました。^[2]

ウォルディンガーは1969年に当時スタンフォード研究所として知られていたSRIインターナショナルに入社し、それ以来ずっとそこにいる。彼は1970年以来、週に2回SRIのオフィスでコーヒーとクッキーを出している。^{[3] [4]}

ウォルディンガーはコーデル・グリーン、ロバート・イェーツ、ジェフ・ルリフソン、ヤン・ダークセンと共同で、自動計画と定理証明を目的としたPLANNER風の人工知能言語である QA4 を開発した。 ^[5] QA4 はコンテキストの概念と結合-可換統一の概念を導入し、これにより演算子の結合公理と可換公理は不要になっただけでなく、表現不可能になった。彼らはこの言語を SRI ロボットShakeyの計画に適用した。ウォルディンガーはバーニー・エルスパスとカール・レビットとともに、プログラム検証（プログラムが想定どおりに動作することを証明すること）に QA4 を使用し、統一アルゴリズムとHoareの FIND プログラムの自動検証を実現した。

ウォルディンガーの論文は、出力を返すが副作用を生じない応用プログラムの合成を扱っていたが、その後、ウォルディンガーは両方を行う命令型プログラムの合成に目を向けた。^{[6]互いに干渉する目標を同時に達成するという問題に対処するために、彼は}フロイド、キング、ホーア、ダイクストラによるプログラム検証の初期の研究から得られた目標回帰の概念を導入した。命令型プログラムは計画に類似しているため、このアプローチは古典的なAI計画問題にも適用できる。

スタンフォード大学のゾハル・マンナと共同で、ウォルディンガーは非節解決法を開発した。これは、論理文を制限された節形式に変換する必要のない解決法である。この変換はコストがかかるだけでなく、結果として得られる定理の証明が病的に複雑になることもあったが、この新しい規則によってこれらの問題は回避された。彼らはこの規則を論文に適用し、統一アルゴリズムの詳細な合成を作成した。別の論文では、彼らは新しい平方根アルゴリズムを合成し、平方根の仕様に解決規則を一度適用するだけで、二分探索の概念が自然に現れることを発見した。^{[7] [8]}

マンナとウォルディンガーの定理証明のアイデアのいくつかは、マーク・スティッケルのSNARK定理証明器の設計に組み込まれました。マイク・ローリー率いるNASAの研究者は、SNARKをソフトウェア開発環境Amphionの実装に使用しました。Amphionは、惑星天文学者向けにNASAミッションのデータを分析するプログラムを作成するために使用されています。Amphionによって自動的に構築されたソフトウェアは、NASAのカッシーニ-ホイヘンスミッションの写真撮影を計画するために使用されました。これは、演繹的方法によって自動的に構築されたソフトウェアのこれまでで最も実用的なアプリケーションである可能性があります。

SNARK システムは、Kestrel Instituteによってソフトウェア開発環境 Specware に組み込まれており、Waldinger はこれを使用してDAML、DARPAエージェント マークアップ言語、およびその後継であるOWLの 1 階公理化を検証しました。SNARK は、DAML の公理だけでなく、DAML 公理化のベースとなった基礎言語KIFの公理にも矛盾があることを明らかにしました。最近、Waldinger は、地理、生物学、およびインテリジェンス分析に関する質問に答えるための演繹法の応用に取り組んでいます。Kestrel Institute と共同で、彼は SNARK を使用してセキュリティ プロトコルを認証しています。

1991年、ウォルディンガーは人工知能推進協会のフェローに選出された。^[9]

私生活では、ウォルディンガーは合気道、ヨガ、瞑想を学んでいます。また、定評のある執筆グループのメンバーでもあり、フードジャーナリズムやエロティックな小説を出版しています。^[10] ウォルディンガーは結婚しており、2人の子供と3人の孫がいます。

• ゲルト・グローセとリチャード・ヴァルディンガー。「同時行為の理論に向けて」EWSP 1991: 78-87。
• ゾハル・マンナとリチャード・ウォルディンガー。「バイナリ検索パラダイムの起源」科学計算プログラム。9(1): 37-83 (1987)

• リチャード・ウォルディンガーのホームページ