Finding hypothetical answers with a resolution theorem prover

Resolution refutation is a powerful reasoning technique employed in many automated theorem provers. Var-ious 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 pro-vide both "intensional " and "extensional " answers to questions by considering a theorem to be proven as a question. An intensional answer is 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 answer is a fact, such as "Rachel detests Fido". The notion of what constitutes an answer can be expanded so that, as resolution pro-ceeds, the intermediate results generated on the way to nding an intensional or extensional answer may be regarded as answers. This view of resolution as answer generation, and resolvants as answers, requires an ex-panded notion of what constitutes an answer. A class of \hypothetical " answers is proposed, having the gen-eral form X) Y, where X can not be proven based on the information in the knowledge base. When there is not enough information in a knowledge base to provide an intensional or extensional answer, a hypothetical answer can be useful