Richard J. Waldinger
Principal Scientist, Artificial Intelligence Center
Richard Waldinger, Ph.D., focuses on applying automatic deduction to artificial intelligence and software engineering. His research areas include program synthesis and verification, and planning. He has studied the use of deductive methods for natural-language question answering, and he is the co-author (with Zohar Manna) of a series of textbooks on the relationship between logic and computer programming.
Waldinger has been with the AIC since 1969 and has worked on theorem proving and its application to automated program synthesis and other problems on the border between software engineering and artificial intelligence. He also has served as a consulting professor of computer science at Stanford University.
He received his Ph.D. from Carnegie Mellon University under Herbert A. Simon. Waldinger is a recipient of an SRI Fellowship, a AAAI Fellowship, and a Herbrand Award.
Recent publications
-
Automating the Derivation of Unification Algorithms. A Case Study in Deductive Program Synthesis
The unification algorithm has long been a target for program synthesis research, but a fully automatic derivation remains a research goal.
-
Natural Language Access: When Reasoning Makes Sense
We argue that to use natural language effectively, we must have both a deep understanding of the subject domain and a general-purpose reasoning capability.
-
What, Again? Automatic Deductive Synthesis of the Unification Algorithm
We describe work in progress towards deriving a unification algorithm automatically from a declarative specification using deductive methods.
-
Deductive Synthesis of the Unification Algorithm: The Automation of Introspection
We are working to create the first automatic deductive synthesis of a unification algorithm. The program is extracted from a proof of the existence of an output substitution that satisfies…
-
Natural Language Access to Data: It Takes Common Sense!
In a deductive approach to this problem, language processing technology translates English queries into a first-order logical form, which is regarded as a conjecture to be established by a theorem…
-
Deduction for Natural Language Access to Data
We outline a general approach to automated natural-language question answering that uses first-order logic and automated deduction. Our interest is in answering queries over structured data resources