• Skip to primary navigation
  • Skip to main content
SRI InternationalSRI mobile logo

SRI International

SRI International - American Nonprofit Research Institute

  • About
    • Blog
    • 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
  • 日本支社
Show Search Search
Hide Search Close
Home » Archives for Richard J. Waldinger

Richard J. Waldinger

SRI Author

  • Richard J. Waldinger

    Principal Scientist, Artificial Intelligence Center

    View all posts

Speech & natural language publications July 27, 2021

Natural Language Access: When Reasoning Makes Sense

Richard J. Waldinger July 27, 2021

Natural language is one of the more appealing ways by which people can interact with computers, but up to now its application has been severely constrained. 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. We illustrate the issues with SAP-QUEST, a proof-of-concept system for natural language question answering over a set of data sources for business enterprise applications, but the argument can be applied more generally to dialogue-style interfaces over a variety of subject domains.

Artificial intelligence publications June 22, 2021 Conference Paper

What, Again? Automatic Deductive Synthesis of the Unification Algorithm

Richard J. Waldinger June 22, 2021

We describe work in progress towards deriving a unification algorithm automatically from a declarative specification using deductive methods. The specification is phrased as a logical theorem and the program is extracted from the proof. The theorem is proved using Stickel’s system SNARK, operating over a theory of expressions and substitutions. The theory has been formulated to allow a simpler specification of the algorithm, and the theorem prover has discovered novelties in the implementation. It is hoped that the same techniques may enable the discovery of previously unknown unification algorithms for specific theories.

Cyber & formal methods publications November 1, 2020

Deductive Synthesis of the Unification Algorithm: The Automation of Introspection

Richard J. Waldinger November 1, 2020

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. Tests are introduced via case analysis in the proof, and recursion by application of the mathematical induction principle. The automation of the proof is challenging because it combines full quantifier reasoning and induction in a single framework. The program obtained is simpler than those previously constructed manually. Improvements in theorem proving technology lead us to believe that deductive synthesis could become a viable part of software production. Also, we suggest that a theorem prover’s reasoning about itself can be regarded as a form of introspection, which may enable it to improve itself.

Artificial intelligence publications March 1, 2015 Conference Paper

Natural Language Access to Data: It Takes Common Sense!

Richard J. Waldinger March 1, 2015

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

SRI International, Richard J. Waldinger January 1, 2014

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

Artificial intelligence publications April 1, 2007 Article

Deductive Biocomputing

Richard J. Waldinger April 1, 2007

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.

Artificial intelligence publications May 1, 2006 Conference Paper

Deductive Discovery and Composition of Resources

Richard J. Waldinger May 1, 2006

We consider the problem of answering a query, where the answer is not provided explicitly by any one resource, but has to be deduced from information provided by many resources; where the resources include both data and software; and where the resources are heterogeneous and not designed to work together. We adopt a deductive approach to this problem, in which the discovery of the appropriate resources and their composition is performed by a theorem prover. The techniques are domain-independent and are applied here to problems in molecular biology. Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC, semantic integration, question answering, bioinformatics, answer extraction, procedural attachment, theorem proving.

Artificial intelligence publications December 1, 1969 Conference Paper

Deductive Coordination of Multiple Geospatial Knowledge Sources

Richard J. Waldinger December 1, 1969

Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC

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

Blog

Institute

Leadership

Press room

Media inquiries

Compliance

Privacy policy

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