World Library  
Flag as Inappropriate
Email this Article

Richard Waldinger

Article Id: WHEBN0012522883
Reproduction Date:

Title: Richard Waldinger  
Author: World Heritage Encyclopedia
Language: English
Subject: Planner (programming language), Structural synthesis of programs, Herbert A. Simon, Scientific community metaphor, SRI International
Publisher: World Heritage Encyclopedia

Richard Waldinger

Richard Waldinger
Nationality American
Institutions SRI International
Alma mater Carnegie Mellon University
Doctoral advisor Herbert A. Simon[1]

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.

Early life and education

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]


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]


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

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]


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 NASA missions for planetary astronomers. Software constructed automatically by Amphion has been used to plan photography for the Cassini-Huygens NASA mission; this is perhaps the most practical application to date of software constructed automatically by deductive methods.

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 DARPA agent markup language, and its successor, OWL. SNARK uncovered inconsistencies not only in the axioms for DAML, but also in the axioms for the foundational language KIF, on which the DAML axiomatization was based. Recently, Waldinger has worked on the application of deductive methods to answer questions in geography, biology, and intelligence analysis. In collaboration with the Kestrel Institute, he has been using SNARK to authenticate security protocols.

Memberships and awards

In 1991, Waldinger was elected as a fellow of the Association for the Advancement of Artificial Intelligence.[9]

Personal life

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.[10]


  1. ^ "Richard Jay Waldinger". AI Genealogy Project. Retrieved 2012-03-15. 
  2. ^ Waldinger, Richard J (1969). Constructing programs automatically using theorem proving (Thesis).  
  3. ^ "Richard Waldinger's Coffee and Cookies".  
  4. ^  
  5. ^  
  6. ^  
  7. ^ Manna, Zohar; Richard Waldinger (1987). "The Deductive Synthesis of Imperative LISP Programs". AAAI: 155–160. 
  8. ^ Manna, Zohar; Richard Waldinger (1993). The Deductive Foundations of Computer Programming. Addison-Wesley. 
  9. ^ "Elected AAAI Fellows".  
  10. ^ "Authors". One Page Stories. Retrieved 2012-03-15. 

Further reading

  • 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 (1987)

External links

  • Richard Waldinger’s home page
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.