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!
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
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. 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.
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. 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
Answering Science Questions: Deduction with Answer Extraction and Procedural Attachment
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.
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.