Richard J. Waldinger
Richard J. Waldinger studies how automated deduction can support programming and question answering. Waldinger has worked at SRI’s Artificial Intelligence Center since 1969 and earned a Carnegie Mellon doctorate under Herbert A. Simon. With Karl N. Levitt, he described a QA4-based program-verification system in 1973. Waldinger coauthored a 2014 paper applying first-order logic and automated deduction to questions over structured data, using a prototype called Quest. His 2025 preprint, revised in 2026, continues work on extracting unification algorithms from constructive proofs. Fully automatic unification derivation remains a research goal.
- Now at
- SRI International
- Works
- 133
- Citations
- 3,512
- h-index
- 28
Publication numbers from OpenAlex, as of 14 October 2026.
Timeline
-
1969; doctorate date unstated
An SRI base for deduction
Waldinger has worked at SRI’s Artificial Intelligence Center since 1969. He earned a Carnegie Mellon doctorate supervised by Herbert A. Simon. His work connects theorem proving with program synthesis, verification and planning.
-
October 1973
Reasoning about programs
With Karl N. Levitt, Waldinger described a theorem prover implemented in QA4. It represented programming concepts such as numbers, arrays and lists and used them in a verification system. The original abstract reports proofs for specific programs and algorithms.
-
2014
Questions over structured data
He coauthored an approach to natural-language access with Condoravdi, Richardson, Sikka and Suenbuel. It maps queries to first-order logic and uses automated deduction over data resources. The Quest prototype illustrates enterprise question answering in a known subject domain. The paper limits its approach to specified resources and background knowledge.
-
August 2025–July 2026
Continuing unification research
Waldinger’s preprint describes extracting a unification algorithm from a constructive proof. It builds on the manual Manna–Waldinger approach and represents earlier substitutions in an environment. The first version appeared in August 2025 and a revision appeared in July 2026. Fully automatic derivation remains a research goal.
Sources and credits
Photo: www.sri.com; Richard J. Waldinger profile photograph; creator not stated. License: Not stated by source. Source: sri.com. Cropped to a square and resized. Ask us to remove or replace this photo.