Richard Jay Waldinger is a computer science researcher at SRI
International's
Contents 1 Early life and education 2 Career 2.1 QA4 2.2 Program synthesis 2.3 SNARK 3 Memberships and awards 4 Personal life 5 References 6 Further reading 7 External links Early life and education[edit]
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.[2]
Career[edit]
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.[3][4]
QA4[edit]
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.[5] 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.
Program synthesis[edit]
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.[6] 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.
In collaboration with Zohar Manna, of Stanford University, Waldinger
developed nonclausal resolution, a form of resolution that did not
require the translation of logical sentences into a restricted clausal
form. Not only was the translation expensive, but also it sometimes
pathologically complicated the proof of the resulting theorem; these
problems were circumvented by the new rule. They applied the rule on
paper to produce a detailed synthesis of a unification algorithm. In a
separate paper, they synthesized a novel square-root algorithm; they
found that the notion of binary search appears spontaneously by a
single application of the resolution rule to the specification of the
square root.[7][8]
SNARK[edit]
Some of Manna and Waldinger's theorem proving ideas were incorporated
into the design of Mark Stickel's SNARK theorem prover. NASA
researchers, led by Mike Lowry, used SNARK in the implementation of
the software-development environment Amphion, which has been used to
construct programs to analyze data from
^ "Richard Jay Waldinger". AI Genealogy Project. Retrieved
2012-03-15.
^ Waldinger, Richard J (1969). Constructing programs automatically
using theorem proving (Thesis).
Further reading[edit] Gerd Große and Richard Waldinger. "Towards a Theory of Simultaneous
Actions" EWSP 1991: 78-87.
External links[edit] Richard Waldi |