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

Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, answer set programming (ASP) and Datalog. In all of these languages, rules are written in the form of clauses:

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> American entrepreneur and researcher in artificial intelligence

Douglas Bruce Lenat is the CEO of Cycorp, Inc. of Austin, Texas, and has been a prominent researcher in artificial intelligence. Lenat was awarded the biannual IJCAI Computers and Thought Award in 1976 for creating the machine-learning program AM. He has worked on machine learning, knowledge representation, "cognitive economy", blackboard systems, and what he dubbed in 1984 "ontological engineering". He has also worked in military simulations, and numerous projects for US government, military, intelligence, and scientific organizations. In 1980, he published a critique of conventional random-mutation Darwinism. He authored a series of articles in the Journal of Artificial Intelligence exploring the nature of heuristic rules.

<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 used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A formal system is essentially an "axiomatic system".

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 automatization. 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.

<span class="mw-page-title-main">Logic in computer science</span> Academic discipline

Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:

Loom is a knowledge representation language developed by researchers in the artificial intelligence research group at the University of Southern California's Information Sciences Institute. The leader of the Loom project and primary architect for Loom was Robert MacGregor. The research was primarily sponsored by the Defense Advanced Research Projects Agency (DARPA).

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 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.

<span class="mw-page-title-main">Wolfgang Bibel</span>

Leonhard Wolfgang Bibel is a German computer scientist, mathematician and Professor emeritus at the Department of Computer Science of the Technische Universität Darmstadt. He was one of the founders of the research area of artificial intelligence in Germany and Europe and has been named as one of the ten most important researchers in the German artificial intelligence history by the Gesellschaft für Informatik. Bibel established the necessary institutions, conferences and scientific journals and promoted the necessary research programs to establish the field of artificial intelligence.

In information technology a reasoning system is a software system that generates conclusions from available knowledge using logical techniques such as deduction and induction. Reasoning systems play an important role in the implementation of artificial intelligence and knowledge-based systems.

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.

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.