Abstract: Identifying that parts of a knowledge base are irrelevant to a specific query is a powerful method of controlling search during problem solving. However, finding methods of such irrelevance reasoning and analyzing their utility are open problems. This paper presents a framework based on a proof-theoretic analysis of irrelevance that enables us to address these problems. Within the framework, we focus on a class of strong-irrelevance claims and show that they have several desirable properties. For example, in the context of Horn-rule knowledge bases, we show that strong-irrelevance claims can be derived efficiently either by examining the KB or as logical consequences of other strong-irrelevance claims. An important aspect is that our algorithms reason about irrelevance using only a small part of the knowledge base. Consequently, the reasoning is efficient and the derived irrelevance claims are independent of changes to other parts of the knowledge base.