Richard Waldinger
Encyclopedia
Richard J. 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.
. 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.
, 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.
. 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 Kestrel 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.
SRI International
SRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later...
's Artificial Intelligence Center
Artificial Intelligence Center
The Artificial Intelligence Center at SRI International was founded in 1966 by Charles Rosen and studies artificial intelligence. One of their early projects was Shakey the Robot, the first general-purpose mobile robot. More recently, the center funded early development of CALO and Siri....
(where he has worked since 1969) whose interests focus on the application of automated deductive reasoning
Deductive reasoning
Deductive reasoning, also called deductive logic, is reasoning which constructs or evaluates deductive arguments. Deductive arguments are attempts to show that a conclusion necessarily follows from a set of premises or hypothesis...
to problems in software engineering
Software engineering
Software Engineering is the application of a systematic, disciplined, quantifiable approach to the development, operation, and maintenance of software, and the study of these approaches; that is, the application of engineering to software...
and artificial intelligence
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
. 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.
Work on QA4
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, ShakeyShakey the Robot
Shakey the Robot was the first general-purpose mobile robot to be able to reason about its own actions. While other robots would have to be instructed on each individual step of completing a larger task, Shakey could analyze the command and break it down into basic chunks by itself...
. 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
Hoare
Hoare may refer to:Individual people* C. A. R. Hoare , British computer scientist* Des Hoare , Australian cricketer* Desmond Hoare , British sailor & educator...
's FIND program.
Work on 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. 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 FloydFloyd
Floyd is either a variant spelling of the Scottish name Flood or the Welsh name Lloyd which means grey, and may refer to:-Places in the United States:* Floyd, Arkansas* Floyd, California **Floyd, Fresno County, California...
, King, Hoare
Hoare
Hoare may refer to:Individual people* C. A. R. Hoare , British computer scientist* Des Hoare , Australian cricketer* Desmond Hoare , British sailor & educator...
, and Dijkstra. Since imperative programs are analogous to plans, the approach was also applicable to classical AI planning problems.
In collaboration with Zohar Manna
Zohar Manna
Zohar Manna is a professor of computer science at Stanford University. He is the author of The Mathematical Theory of Computation , one of the first texts to provide extensive coverage of the mathematical concepts behind computer programming.With Amir Pnueli, he co-authored an unfinished trilogy...
, of Stanford University
Stanford University
The Leland Stanford Junior University, commonly referred to as Stanford University or Stanford, is a private research university on an campus located near Palo Alto, California. It is situated in the northwestern Santa Clara Valley on the San Francisco Peninsula, approximately northwest of San...
, 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.
Work on SNARK
Some of Manna and Waldinger's theorem proving ideas were incorporated into the design of Mark Stickel's SNARK theorem proverSNARK theorem prover
SNARK, , is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering....
. NASA
NASA
The National Aeronautics and Space Administration is the agency of the United States government that is responsible for the nation's civilian space program and for aeronautics and aerospace research...
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
Cassini-Huygens
Cassini–Huygens is a joint NASA/ESA/ASI spacecraft mission studying the planet Saturn and its many natural satellites since 2004. Launched in 1997 after nearly two decades of gestation, it includes a Saturn orbiter and an atmospheric probe/lander for the moon Titan, although it has also returned...
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 Kestrel 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
Web Ontology Language
The Web Ontology Language is a family of knowledge representation languages for authoring ontologies.The languages are characterised by formal semantics and RDF/XML-based serializations for the Semantic Web...
. SNARK uncovered inconsistencies not only in the axioms for DAML, but also in the axioms for the foundational language KIF
KIF
KIF may stand for:* Knowledge Interchange Format* Kingfisher Lake Airport's IATA code* Københavns Idræts Forening, Denmark's oldest athletics club* KIF Kolding, a team handball club based in Kolding, Denmark...
, 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.