  When proving theorems from large sets of logical assertions, it can be
helpful to restrict the search for a proof to those assertions that are
relevant, that is, closely related to the theorem in some sense. For example,
in the Watson system, a large knowledge base must rapidly be searched for
relevant facts. It is possible to define formal concepts of relevance for
propositional and first-order logic. Various concepts of relevance have been
defined for this, and some have yielded good results on large problems. We
consider here in particular a concept based on alternating paths.We present
efficient graph-based methods for computing alternating path relevance and give
some results indicating its effectiveness. We also propose an alternating path
based extension of this relevance method to DPLL with an improved time bound,
and give other extensions to alternating path relevance intended to improve its
performance.

Logic in Computer Science;Artificial Intelligence