Successful Horn clause derivations are finite trees and this leads to a straightforward correspondence between a set of Horn clauses and a finite tree automaton. In the talk the role of this connection in Horn clause analysis and verification is explained, including elimination of failing derivations and refinement of abstractions. We also briefly outline an optimised algorithm for determinisation of finite tree automata, which plays a role in this work.