A note on Dowling-Gallier's Top-Down algorithm for Propositional Horn Satisfiability