A question-answering interpretation of resolution refutation
Debra T. Burhans, Stuart C. Shapiro · 2002
Early use of theorem provers for question answering identified the presence of an answer with proof. Later work recognized other types of answers whose existence was not associated with proof, including intensional and conditional answers. This work is concerned with the problem of defining what is meant by answer in the context of resolution theorem proving. Clauses that are relevant are all identified as answers, where relevance is determined with respect to a question and knowledge base: any clause descended from the negated question is deemed relevant. This definition of relevance is not in and of itself novel; rather, it is the way in which the set of relevant clauses is partitioned that provides the key to interpreting clauses as answers. A partition that divides the set of relevant clauses into three classes, termed specific, generic , and hypothetical, is proposed. These classes are formally distinguished by the way in which literals in a clause share variables, with class membership based on a property termed the closure of variable sharing of a literal. The best answers are identified with relevant clauses that are, additionally, informative. The informativeness of a clause is determined with respect to a set of clauses termed the answer set, where an informative clause contains information not conveyed by any other clause in the set. The process of reasoning in search of a proof is recast as the process of constructing a sequence of answer sets, starting with the empty set, where each set in the sequence is at least as informative as the previous set. It is this property that identifies question answering as an anytime reasoning process. The complete answer set for a given question and knowledge base is shown to be the fixed point of the answer set generation function. The complete characterization of resolvents as answers presented herein provides a framework that formalizes and expands upon previous work on question answering in a resolution theorem prover. In addition, it provides a foundation for further work by establishing a context-independent logical pragmatics of question answering.