Author: Richard J. Waldinger
-
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 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.