An Efficient Relevance Criterion for Mechanical Theorem Proving

David A. Plaisted

To solve problems in the presence of large knowledge bases, it is important to be able to decide which knowledge is relevant to the problem at hand. This issue is discussed in [1, see paper]. We present efficient algorithms for selecting a relevant subset of knowledge. These algorithms are presented 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 strategy which selects at each step the resolvents that appear most relevant. This strategy is compatible with arbitrary conventional strategies such as P-deduction, locking resolution, et cetera. Also, this strategy uses nontrivial semantic information and "associations" between facts in a way similar to human problem-solving processes.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.