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. An algorithm previously introduced is improved by changing the input formula before running it. This enlarges the restriction that makes the algorithm polynomial and decreases its running time in other cases. The size of the resulting formula decreases consequently.