# Properties and Extensions of Alternating Path Relevance - I

## TL;DR

This paper explores the concept of alternating path relevance in logical theorem proving, presenting efficient graph-based computation methods and extensions to improve relevance filtering in large logical systems.

## Contribution

It introduces a novel alternating path relevance concept, along with efficient algorithms and extensions for DPLL, enhancing relevance-based theorem proving.

## Key findings

- Efficient graph-based algorithms for computing alternating path relevance.
- Extensions to DPLL improve relevance filtering performance.
- Results indicate effectiveness in large problem instances.

## Abstract

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.