Theorem Provers as Question Answerers

Abstract

This paper describes a deductive question-answering computer program that uses the Robinson resolution procedure to perform logical inferences and retrieve facts on the basis of a fairly large body of stored data. Irrelevant searches and inferences are kept to a minimum by means of some recently developed theorem-proving techniques, most notably Meltzer's 1 Pl-deduction with set of support' and the 'first-literal resolution' method of Hayes and Kowalski, together with a dictionary listing of the premises in the data base in terms of the predicates and other key constants of their first literals. Using the special predicate Var of Green and Raphael, the program can handle questions requiring a list of answers, such as 'which (or how many) individuals satisfy a condition 0?', as well as simpler questions requiring a single answer, , such as 'is individual~ a 0?' In a series of tests using a data base containing the names and party affiliations of the senators, congressmen and governors of the fifty American states, the program has shown the ability to perform fairly complex deductions efficiently in the presence of a large number of irrelevant premises.