Richard Waldinger
| Richard Waldinger | |
|---|---|
| Nationality | American |
| Institutions | SRI International |
| Alma mater | Carnegie Mellon University |
| Doctoral advisor | Herbert A. Simon |
Richard Jay Waldinger is a computer science researcher at SRI International's Artificial Intelligence Center (where he has worked since 1969) whose interests focus on the application of automated deductive reasoning to problems in software engineering and artificial intelligence.
In his thesis (Carnegie Mellon University, 1969), which concerned the extraction of computer programs from proofs of theorems, he found that the application of the resolution rule accounted for the appearance of a conditional branch in the extracted program, while the use of the mathematical induction principle caused the introduction of recursion and other repetitive constructs.
Waldinger started at SRI International, then known as the Stanford Research Institute, in 1969, and has remained there since then. He has served coffee and cookies in his office at SRI twice a week since 1970.
Waldinger collaborated with Cordell Green, Robert Yates, Jeff Rulifson, and Jan Derksen on QA4, a PLANNER-like artificial intelligence language geared towards automatic planning and theorem proving. QA4 introduced the notion of context and also of associative-commutative unification, which made the associative and commutative axioms for operators not only unnecessary but also inexpressible. They applied the language to planning for the SRI robot, Shakey. With Bernie Elspas and Karl Levitt, Waldinger used QA4 for program verification (proving that a program does what it's supposed to), obtaining automatic verifications for the unification algorithm and Hoare's FIND program.
While Waldinger's thesis had dealt with the synthesis of applicative programs, which return an output but produce no side effects, Waldinger then turned to the synthesis of imperative programs, which do both. To deal with the problem of achieving simultaneously goals that interfere with each other, he introduced the notion of goal regression, which was obtained from earlier work in program verification by Floyd, King, Hoare, and Dijkstra. Since imperative programs are analogous to plans, the approach was also applicable to classical AI planning problems.
...
Wikipedia