One head is better than two: a polynomial restriction for propositional definite Horn forgetting

It is NPcomplete even in one of the simplest cases: propositional definite Horn [Lib20a]. A way to forget variables from a definite Horn formula is to recursively replace them [Lib20a]. Forgetting from general Horn formulae can be done by turning the formula definite Horn before forgetting and adding some clauses afterwards [Lib20a]. Therefore, while this article concentrates on definite Horn formulae, the results apply to the general Horn case. In particular, it shows how efficiency increases by modifying the input formula before running the replacement algorithm.