  Logical forgetting may take exponential time in general, but it does not when
its input is a single-head propositional definite Horn formula. Single-head
means that no variable is the head of multiple clauses. An algorithm to make a
formula single-head if possible is shown. It improves over a previous one by
being complete: it always finds a single-head formula equivalent to the given
one if any.
