Author: Richard J. Waldinger

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

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

  • 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

  • English Access to Structured Data

    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.

  • Deductive Formation of Recursive Workflows

    We present an action theory with the power to represent recursive plans and the capability to reason about and synthesize recursive workflow control structures.

  • Answering Science Questions: Deduction with Answer Extraction and Procedural Attachment

    An approach to question answering through automated deduction is advocated. External knowledge resources, including data and software, are consulted through a mechanism known as procedural attachment.

  • Deductive Biocomputing

    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.

  • Whatever Happened to Deductive Question Answering?

    Program synthesis as a byproduct of automatic theorem proving has been a largely dormant field in recent years, while those seeking to apply theorem proving have been scurrying to find smaller problems, including question answering.

  • Proving Authentication Properties in the Protocol Derivation Assistant

    In the present paper, we introduce an axiomatic theory of authentication suitable for the automatic proof of authentication properties. We describe a proof of the authentication property of a simple protocol, as derived in Pda, for which the the proof obligations have been automatically generated and discharged.

  • Deductive Discovery and Composition of Resources

    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.