• Skip to primary navigation
  • Skip to main content
SRI logo
  • About
    • Press room
  • Expertise
    • Advanced imaging systems
    • Artificial intelligence
    • Biomedical R&D services
    • Biomedical sciences
    • Computer vision
    • Cyber & formal methods
    • Education and learning
    • Innovation strategy and policy
    • National security
    • Ocean & space
    • Quantum
    • QED-C
    • Robotics, sensors & devices
    • Speech & natural language
    • Video test & measurement
  • Ventures
  • NSIC
  • Careers
  • Contact
  • 日本支社
Search
Close
Home » Archives for Richard J. Waldinger
Richard J. Waldinger

Richard J. Waldinger

Principal Scientist, Artificial Intelligence Center
Go to bio page

Publications

Speech & natural language publications July 27, 2021

Natural Language Access: When Reasoning Makes Sense

Richard J. Waldinger

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.

Artificial intelligence publications June 22, 2021

What, Again? Automatic Deductive Synthesis of the Unification Algorithm

Richard J. Waldinger

We describe work in progress towards deriving a unification algorithm automatically from a declarative specification using deductive methods.

Cyber & formal methods publications November 1, 2020

Deductive Synthesis of the Unification Algorithm: The Automation of Introspection

Richard J. Waldinger

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 a given logical specification.

Artificial intelligence publications March 1, 2015 Conference Paper

Natural Language Access to Data: It Takes Common Sense!

Richard J. Waldinger

Commonsense reasoning proves to be an essential tool for natural-language access to data. 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 prover. Subject domain knowledge is encoded in an axiomatic theory equipped with links to appropriate databases. Commonsense reasoning is necessary to disambiguate the query, to connect the query with relevant tables in the databases, to deal with logical relationships in the query, and to achieve interoperability between disparate databases. This is illustrated with examples from the Quest system, which deals with queries over business enterprise data. Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC

Speech & natural language publications January 1, 2014 Conference Paper

Deduction for Natural Language Access to Data

Richard J. Waldinger, SRI International

Knowledge and reasoning in a specific subject domain can greatly assist in natural language processing. This is demonstrated in the context of QUEST, a question answering system for accessing data for business enterprise software. Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC, natural language, question answering, deduction, theorem proving, databases, answer extraction, procedural attachment

Speech & natural language publications January 1, 2011 Conference Paper

English Access to Structured Data

Richard J. Waldinger

We present work on using a domain model to guide text interpretation, in the context of a project that aims to interpret English questions as a sequence of queries to be answered from structured databases. We adapt a broad-coverage and ambiguity-enabled natural language processing (NLP) system to produce domain-specific logical forms, using knowledge of the domain to zero in on the appropriate interpretation. The vocabulary of the logical forms is drawn from a domain theory that constitutes a higher-level abstraction of the contents of a set of related databases. The meanings of the terms are encoded in an axiomatic domain theory. To retrieve information from the databases, the logical forms must be instantiated by values constructed from fields in the database. The axiomatic domain theory is interpreted by the first-order theorem prover SNARK to identify the groundings, and then retrieve the values through procedural attachments semantically linked to the database. SNARK attempts to prove the logical form as a theorem by reasoning over the theory that is linked to the database and returns the exemplars of the proof(s) back to the user as answers to the query. The focus of this paper is more on the language task; however, we discuss the interaction that must occur between linguistic analysis and reasoning for an end-to-end natural language interface to databases. We illustrate the process using examples drawn from an HIV treatment domain, where the underlying databases are records of temporally bound treatments of individual patients. Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC, Natural language processing, Natural language interfaces to databases, Deductive question answering, Theorem proving, HIV drug resistance database.

Artificial intelligence publications September 1, 2009 Article

Deductive Formation of Recursive Workflows

Richard J. Waldinger

We present an action theory with the power to represent recursive plans and the capability to reason about and synthesize recursive workflow control structures. In contrast with the software verification setting, reasoning does not take place solely over predefined data structures, and neither is there a process specification available in recursive form. Rather, specification takes the form of goals, and domain structure takes the form of a physical application setting containing objects. For this reason, well-founded induction is employed for its suitability for practical action domains where recursive structures must be described or inferred. Under this method, termination of the synthesized recursive workflow is a property that follows automatically. We show how a general workflow recursive construct is added to an action language that is then augmented with induction. This formalism is then transformed in a way amenable to automated reasoning. We demonstrate the method with a particular example specified in the theory, and then extracted from a proof constructed by the SNARK first-order theorem prover. Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC, workflow, recursive plans, theorem proving, well-founded induction, resolution, action theory, program extractio, termination

Artificial intelligence publications January 1, 2008 Conference Paper

Answering Science Questions: Deduction with Answer Extraction and Procedural Attachment

Richard J. Waldinger

An approach to question answering through automated deduction is advocated. Answers to questions are extracted from proofs of associated conjectures over an axiomatic theory of the subject domain. External knowledge resources, including data and software, are consulted through a mechanism known as procedural attachment.

Artificial intelligence publications April 1, 2007 Article

Deductive Biocomputing

Richard J. Waldinger

Background: As biologists increasingly rely upon computational tools, it is imperative that they be able to appropriately apply these tools and clearly understand the methods the tools employ. Such tools must have access to all the relevant data and knowledge and, in some sense, “understand” biology so that they can serve biologists’ goals appropriately and “explain” in biological terms how results are computed. Methodology/Principal Findings: We describe a deduction-based approach to biocomputation that semiautomatically combines knowledge, software, and data to satisfy goals expressed in a high-level biological language. The approach is implemented with the help of an automatic theorem prover equipped with a web-based biocomputing platform called BioDeducta, which combines SRI’s SNARK theorem prover with the BioBike interactive integrated knowledge base. The biologist/user expresses a high-level conjecture, representing a biocomputational goal query, without indicating how this goal is to be achieved. A subject domain theory, represented in SNARK’s logical language, transforms the terms in the conjecture into capabilities of the available resources and the background knowledge necessary to link them together. If the subject domain theory enables SNARK to prove the conjecture—that is, to find paths between the goal and BioBike resources—then the resulting proofs represent solutions to the conjecture/query. Such proofs provide provenance for each result, indicating in detail how they were computed. We demonstrate BioDeducta by showing how it can approximately replicate a previously published analysis of genes involved in the adaptation of cyanobacteria to different light niches. Conclusions/Significance: Through the use of automated deduction guided by a biological subject domain theory, this work is a step towards enabling biologists to conveniently and efficiently marshal integrated knowledge, data, and computational tools toward resolving complex biological queries. Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC, knowledge integration, theorem proving, semantic web, bioinformatics, question answering, biocomputing, procedural attachment, answer extraction.

  • Go to page 1
  • Go to page 2
  • Go to page 3
  • Interim pages omitted …
  • Go to page 5
  • Go to Next Page »

How can we help?

Once you hit send…

We’ll match your inquiry to the person who can best help you.

Expect a response within 48 hours.

Career call to action image

Make your own mark.

Search jobs

Our work

Case studies

Publications

Timeline of innovation

Areas of expertise

Institute

Leadership

Press room

Media inquiries

Compliance

Careers

Job listings

Contact

SRI Ventures

Our locations

Headquarters

333 Ravenswood Ave
Menlo Park, CA 94025 USA

+1 (650) 859-2000

Subscribe to our newsletter


日本支社
SRI International
  • Contact us
  • Privacy Policy
  • Cookies
  • DMCA
  • Copyright © 2022 SRI International