most one positive literal per term; similarly, that of Horn-renamable DNFs, i.e., those that can be turned into a Horn DNF by replacing some variables with their negation, and simplifying double negations, everywhere in the formula; 2DNFs, those DNFs with at most two literals per term. We omit the proof of the following proposition, since it is essentially the same as that of Proposition 2 (simply follow the execution of the algorithm).

Proposition 4 Let D be a class of DNFs that is stable under removal of occurrences of literals and for which the TAUTOLOGY problem is polynomial. If E is restricted to belong to D, α is a clause and A is a subset of Var(Σ), then searching for a best explanation for I = (E, a, A) can be done in polynomial time. Thus we can establish that abduction is tractable if (among others) Σ is in Horn-renamable DNF (including the Horn and reverse Horn cases) or in 2DNF, and α is a clause.

Finally, let us point out that with a very similar proof we can obtain polynomiality for some problems obtained by strengthening the restriction of Proposition 4 over Σ, but weakening that over α.

Proposition 5 If Σ is represented by a Horn (resp. reverse Horn) DNF of k terms and α by a positive (resp. negative) CNF of k' clauses, and A is a subset of Var(Σ), then searching for a best explanation for Π = (Σ, α, Α) can be done in time Ο(( k + [ A ]) kk ′ n).

The same holds if Σ is represented by a positive (resp. negative) DNF of k terms and α by a Horn (resp. reverse Horn) CNF of k' clauses.

Once again note that variables, literals and terms are all special cases of (reverse) Horn CNFs, and that variables, positive (resp. negative) clauses and positive (resp. negative)
terms are all special cases of positive (resp. negative) CNFs.

## 7. Discussion And Perspectives

The general algorithm presented in this note allows us to derive new polynomial restrictions of abduction problems; even if this is not discussed here, for lack of space, it also allows to unify some previously known such restrictions (such as Σ in 2CNF and α in 2DNF, or Σ
in monotone CNF and α given as a clause). The following list summarizes the main new polynomial restrictions:
- Σ given as an affine formula and α as a disjunction of linear equations (Proposition 2) - Σ in Horn-renamable DNF and α given as a clause (Proposition 4) - Σ in 2DNF and α given as a clause (Proposition 4)

- Σ in Horn (reverse Horn) DNF and α in positive (negative) CNF (Proposition 5)
- Σ in negative (positive) DNF and α in reverse Horn (Horn) CNF (Proposition 5).

Moreover, even if there is no guarantee for efficiency in the general case the presentation of our algorithm does not depend on the syntactic form of Σ or α , and it uses only standard operations on Boolean functions (projection, conjunction, negation).