Finding Hypothetical Answers with a Resolution Theorem Prover

Resolutionre futation is a powerful reasoning technique employed in many automated theorem provers. Various enhancements to resolution have enabled it to be used as a general question answering mechanism. Question answering systems employing resolution as the basic reasoning technique have been used to provide both "intensional" and "extensional" answers to questions by considering a theorem to be proven as a question. Anintensional answeris a rule, such as "for all x and for all y if x is a cat and y is a dog then x detests y', and an extensional answeris a fact, such as "Rachel detests Fido". Thenotion of what constitutes an answercan be expandedso that, as resolution proceeds, the intermediate results generated on the way to finding an intensional or extensional answermaybe regarded as answers. This view of resolution as answer generation, and resolvants as answers, requires an expanded notion of what constitutes an answer. A class of "hypothetical" answersis proposed, having the general form X = Y, where X can not be proven based on the information in the knowledgebase. Whenthere is not enough in formation in a knowledgebase to provide an intensional or extensional answer, a hypothetical answercan be useful.