ContactPerson: burhans@cse.buffalo.edu
### Begin Citation ### Do not delete this line ###
%R 2002-03
%U /projects/burhans/debra.ps
%A Burhans, Debra T.
%T A Question Answering Interpretation of Resolution Refutation
%D January 31, 2002
%I Department of Computer Science and Engineering, SUNY Buffalo
%K theorem proving, question answering
%X Early use of theorem provers for question answering identified the 
presence of an answer with the presence of a 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.  While this potentially infinite set
may never be realized by a reasoner, the current answer set is
guaranteed to contain the most informative, relevant clauses
available at any point during reasoning.  Different control
structures give rise to different answer set sequences, and may be
selectively employed to generate preferred answers as quickly as
possible.  The definition of answer sets elucidates the importance of
separating answer search from answer selection, and highlights the
subjectivity of the notion of best answer as defined in many question
answering systems.  The complete characterization of resolvents as
answers presented herein provides a framework that accounts for and
expands upon previous work on question answering in a resolution
theorem prover.  In addition, it provides a foundation for further
work in question answering by establishing a context-independent
logical pragmatics of question answering.