One head is better than two: a polynomial restriction for propositional
  definite Horn forgetting
  Logical forgetting is NP-complete even in the simple case of propositional
Horn formulae, and may exponentially increase their size. A way to forget is to
replace each variable to forget with the body of each clause whose head is the
variable. It takes polynomial time in the single-head case: each variable is at
most the head of a clause. Some formulae are not single-head but can be made so
to simplify forgetting. They are single-head equivalent. The first contribution
of this article is the study of a semantical characterization of single-head
equivalence. Two necessary conditions are given. They are sufficient when the
formula is inequivalent: it makes two sets of variables equivalent only if they
are also equivalent to their intersection. All acyclic formulae are
inequivalent. The second contribution of this article is an incomplete
algorithm for turning a formula single-head. In case of success, forgetting
becomes possible in polynomial time and produces a polynomial-size formula,
none of which is otherwise guaranteed. The algorithm is complete on
inequivalent formulae.
