query (another closed formula) is obtained by applying the inference rules to the knowledge base and the logical axioms of the theory.

A formula φ of the knowledge base is irrelevant to the derivation of another formula ψ if φ does not "participate" to the process of inferring ψ from the knowledge base. For example, in the knowledge base {A(1), C(2), A(X) ⇒ B(X)}, it is clear that A(1) is relevant to B (1), while C (2) is not.

This definition becomes complicated when more complex scenarios are considered.  Namely, Levy et al. consider three different "coordinates": first, whether all derivations are considered or just one; second, whether we consider all derivations or just minimal ones; third, whether we consider membership to the proof or just derivability from the formulas that compose the proof (in this case, we have four possible choices).

Besides the fact that this notion of irrelevance is based on first-order logic, there are other, more substantial, differences between it and the ideas investigated in this paper. First, it is a relation between two formulas, given a background knowledge base. As such, it is more related to other notions of relevance in the literature (Lang & Marquis, 1998a).

Second, it is based on the concept of proof, which is something not completely dependent on the semantics. For example, replacing the usual modus ponens with the strange inference rule α,β,α ⇒ γ → γ, which does not change the semantics of the logics, then the formula C (2) of the knowledge base above becomes magically relevant to B (1). This is perfectly reasonable in the approach by Levy et al., where improving efficiency using a specific proof theory is the aim.

## 6.2 Extending Our Notions And Results

The notions and results presented in this paper can be extended in several directions. 6.2.1 NUMERICAL AND ORDINAL NOTIONS OF FORMULA-VARIABLE INDEPENDENCE;
FORGETTING IN MORE GENERAL STRUCTURES
It may be worth wondering about how the notions of FL-independence and FV-independence can be generalized to the case where the knowledge base is not a mere propositional formula but a probability distribution over Ω PS ; or an incomplete probability (or equivalently a set of probability distributions), or a stratified knowledge base, or any other ordinal or nmmerical structure.

First, let us notice that some of our characterizations lead to quite intuitive and general ideas. To take the case of FV-independence, we have shown that the following three statements are equivalent when Σ is a propositional knowledge base:
(a) Σ does not tell anything about x, in any context;
(b) Σ can be rewritten equivalently in a formula Σ′ in which x does not appear
(Definition 4): (c) for any two interpretations ω and ω ′ that differ only in the value given to x, the status of ω with respect to Σ (i.e., model or countermodel) is the same as that of ω ′ (Corollary 1).

As to variable forgetting:
(d) ForgetVar(Σ, V) is the most general consequence of Σ that is Var-independent from V (Corollary 16).