Richard Waldinger

Last updated
Richard Waldinger
Nationality American
Alma mater Carnegie Mellon University
Scientific career
Institutions SRI International
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.

Contents

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]

Career

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

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]

SNARK

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] He is married and has two children and three grandchildren.

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

Knowledge representation and reasoning is the field of artificial intelligence (AI) dedicated to representing information about the world in a form that a computer system can use to solve complex tasks such as diagnosing a medical condition or having a dialog in a natural language. Knowledge representation incorporates findings from psychology about how humans solve problems and represent knowledge, in order to design formalisms that will make complex systems easier to design and build. Knowledge representation and reasoning also incorporates findings from logic to automate various kinds of reasoning.

Planner is a programming language designed by Carl Hewitt at MIT, and first published in 1969. First, subsets such as Micro-Planner and Pico-Planner were implemented, and then essentially the whole language was implemented as Popler by Julian Davies at the University of Edinburgh in the POP-2 programming language. Derivations such as QA4, Conniver, QLISP and Ether were important tools in artificial intelligence research in the 1970s, which influenced commercial developments such as Knowledge Engineering Environment (KEE) and Automated Reasoning Tool (ART).

<span class="mw-page-title-main">Jeff Rulifson</span> American computer scientist

Johns Frederick (Jeff) Rulifson is an American computer scientist.

<span class="mw-page-title-main">Douglas Lenat</span> Computer scientist and AI pioneer

Douglas Bruce Lenat was an American computer scientist and researcher in artificial intelligence who was the founder and CEO of Cycorp, Inc. in Austin, Texas.

Inferences are steps in reasoning, moving from premises to logical consequences; etymologically, the word infer means to "carry forward". Inference is theoretically traditionally divided into deduction and induction, a distinction that in Europe dates at least to Aristotle. Deduction is inference deriving logical conclusions from premises known or assumed to be true, with the laws of valid inference being studied in logic. Induction is inference from particular evidence to a universal conclusion. A third type of inference is sometimes distinguished, notably by Charles Sanders Peirce, contradistinguishing abduction from induction.

<span class="mw-page-title-main">Symbolic artificial intelligence</span> Methods in artificial intelligence research

In artificial intelligence, symbolic artificial intelligence is the term for the collection of all methods in artificial intelligence research that are based on high-level symbolic (human-readable) representations of problems, logic and search. Symbolic AI used tools such as logic programming, production rules, semantic nets and frames, and it developed applications such as knowledge-based systems, symbolic mathematics, automated theorem provers, ontologies, the semantic web, and automated planning and scheduling systems. The Symbolic AI paradigm led to seminal ideas in search, symbolic programming languages, agents, multi-agent systems, the semantic web, and the strengths and limitations of formal knowledge and reasoning systems.

A formal system is an abstract structure and formalization of an axiomatic system used for inferring theorems from axioms by a set of inference rules.

In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both fields make use of formal proof techniques, and both comprise approaches of different degrees of automation. In contrast to automatic programming techniques, specifications in program synthesis are usually non-algorithmic statements in an appropriate logical calculus.

Zohar Manna was an Israeli-American computer scientist who was a professor of computer science at Stanford University.

In computer science, the scientific community metaphor is a metaphor used to aid understanding scientific communities. The first publications on the scientific community metaphor in 1981 and 1982 involved the development of a programming language named Ether that invoked procedural plans to process goals and assertions concurrently by dynamically creating new rules during program execution. Ether also addressed issues of conflict and contradiction with multiple sources of knowledge and multiple viewpoints.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation-complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

A deductive language is a computer programming language in which the program is a collection of predicates ('facts') and rules that connect them. Such a language is used to create knowledge based systems or expert systems which can deduce answers to problem sets by applying the rules to the facts they have been given. An example of a deductive language is Prolog, or its database-query cousin, Datalog.

SNARK, , is a theorem prover for multi-sorted first-order logic intended for applications in artificial intelligence and software engineering, developed at SRI International.

Structural synthesis of programs (SSP) is a special form of (automatic) program synthesis that is based on propositional calculus. More precisely, it uses intuitionistic logic for describing the structure of a program in such a detail that the program can be automatically composed from pieces like subroutines or even computer commands. It is assumed that these pieces have been implemented correctly, hence no correctness verification of these pieces is needed. SSP is well suited for automatic composition of services for service-oriented architectures and for synthesis of large simulation programs.

BioBike(nee. BioLingua ) is a cloud-based, through-the-web programmable (Paas) symbolic biocomputing and bioinformatics platform that aims to make computational biology, and especially intelligent biocomputing accessible to research scientists who are not expert programmers.

Inductive programming (IP) is a special area of automatic programming, covering research from artificial intelligence and programming, which addresses learning of typically declarative and often recursive programs from incomplete specifications, such as input/output examples or constraints.

Mark E. Stickel was a computer scientist working in the fields of automated theorem proving and artificial intelligence. He worked at SRI International for over 30 years, and was Principal Scientist at the Artificial Intelligence Center.

James Robert Slagle was an American computer scientist notable for his many achievements in Artificial Intelligence. Since 1984 he has been the Distinguished Professor of Computer Science at the University of Minnesota, Minneapolis, with former appointments at Johns Hopkins University, the National Institutes of Health, the Naval Research Laboratory, Lawrence Livermore Radiation Laboratory, University of California, Berkeley, and the Massachusetts Institute of Technology.

References

  1. ↑ "Richard Jay Waldinger". AI Genealogy Project. Retrieved 2012-03-15.
  2. ↑ Waldinger, Richard J (1969). Constructing programs automatically using theorem proving (Thesis). Carnegie Mellon University Department of Computer Science.
  3. ↑ "Richard Waldinger's Coffee and Cookies". Artificial Intelligence Center . Retrieved 2012-03-15.
  4. ↑ Nils J. Nilsson (1984). "Introduction to the COMTEX Microfiche Edition of the SRI Artificial Intelligence Center Technical Notes". AI Magazine. Vol. 5, no. 1. p. 46.
  5. ↑ Jeff Rulifson; Jan Derksen; Richard Waldinger (November 1973). "QA4, A Procedural Calculus for Intuitive Reasoning". SRI AI Center Technical Note 73.
  6. ↑ Zohar Manna; Richard Waldinger (1978). "Is "Sometime" Sometimes Better Than "Always"? (Intermittent Assertions in Proving Program Correctness)". Communications of the ACM. 21 (2): 159–172. doi: 10.1145/359340.359353 . S2CID   5905332.
  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". Association for the Advancement of Artificial Intelligence . Retrieved 2012-03-15.
  10. ↑ "Authors". One Page Stories. Retrieved 2012-03-15.

Further reading

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.