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.
Richard J. Waldinger
SRI Author
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. 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.
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. 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.
Natural Language Access to Data: It Takes Common Sense!
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
Deduction for Natural Language Access to Data
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
Deductive Biocomputing
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 SRIs 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 SNARKs 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 conjecturethat is, to find paths between the goal and BioBike resourcesthen 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.
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. 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.
Deductive Coordination of Multiple Geospatial Knowledge Sources
Keywords: Artificial Intelligence, Artificial Intelligence Center, AIC
