An Efficient Relevance Criterion for Mechanical Theorem Proving

Abstract

To solve problems in the presence of large knowledge bases, it is important to be able to de-cide which knowledge is relevant to the problem at hand. This issue is discussed in [l 1. We pre-sent efficient algorithms for selecting a relevant subset of knowledge. These algorithms are presene ed in terms of resolution theorem proving in the first-order predicate calculus, but the concepts are sufficiently general to apply to other logics and other inference rules as well. These ideas should be particularly important when there are tens or hundreds of thousands of input clauses. We also present a complete theorem proving strate-gy which selects at each step the resolvents that appear most relevant. Thisstrategy is compatible with arbitrary conventional strategies such as P-deduction, locking resolution, et cetera. Also, 1 this strategy uses nontrivial semantic information and "associations " between facts in a to human problem-solving processes. I RELEVANCE FUNCTIONS Definition. A support set for a set S of clauses is a subset Ti of S such that S-Ti is con-way similar sistent. A support class for S is a set {Tl,..., Tk] of support sets for S. Definition. A (resolution) proof of C from S is a sequence C1,C2,...,C, of clauses in which Cn is C and each clause C i is either an element of S (an input clause) or a resolvent of two preceding clauses in S. (Possibly both parents of Ci are identical.) The length of such a refutation is n. A refutation from S is a proof of NIL (the empty clause) from S. Definition. A relevance function is a func-tion R which, given a set S of clauses, a support class T for S, and an integer n, maps onto a sub-set Rn(S, T) of S having the following property: If there is a length n refutation from S, then there is a refutation from Rn(S, T) of length n or less. Thus if we are searching for length n refutations from S, we need only search for length n refuta-* This research was partially supported by the Na-