RICHARD JAY WALDINGER is a computer science researcher at SRI
Artificial Intelligence Center
* 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
In his thesis (
Carnegie Mellon University
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.
In collaboration with
Zohar Manna , of
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
The SNARK system has been incorporated by the Kestrel Institute into
their software development environment Specware, which has been used
by Waldinger for the validation of the first-order axiomatization of
DAML , the
MEMBERSHIPS AND AWARDS
In 1991, Waldinger was elected as a fellow of the Association for the Advancement of Artificial Intelligence .
In his personal life, Waldinger is a student of aikido, yoga, and meditation. A member of an established writing group, he has published food journalism and erotic fiction. He is married and has two children and three grandchildren.
* ^ "Richard Jay Waldinger". AI Genealogy Project. Retrieved
* ^ Waldinger, Richard J (1969). Constructing programs
automatically using theorem proving (Thesis). Carnegie Mellon
University Department of Computer Science .
* ^ "Richard Waldinger\'s Coffee and Cookies". Artificial
Intelligence Center . Retrieved 2012-03-15.
Nils J. Nilsson (1984). "Introduction to the COMTEX Microfiche
Edition of the SRI
Artificial Intelligence Center
* Gerd Große and Richard Waldinger. "Towards a Theory of Simultaneous Actions" EWSP 1991: 78-87. * Zohar Manna and Richard Waldinger. "The Origin of a Binary-Search Paradigm" Sci. Comput. Program. 9(1): 37-83