Good characterization of unsatisfiable Horn3SAT formula?
You should not expect a proof that is asymptotically shorter than the formula itself.  For instance, consider

$$(x_1 \implies x_2) \land (x_2 \implies x_3) \land \dots \land (x_{n-1} \implies x_n) \land x_1 \land \neg x_n.$$

This formula is not satisfiable, but any proof of unsatisfiability will need to have size $\Omega(n)$.

If you're willing to accept a "proof" of size $n$, then the formula itself arguably qualifies as a proof (as it's easy to check that a given formula is not satisfiable).

Alternatively, any chain of deductions that ends in a contradiction qualifies as a proof, where each step in the chain is a variable and its inferred truth value, as justified by a clause in the Horn3SAT formula and previously inferred variable truth values.  If the formula is not satisfiable, then there must exist such a chain of deductions of size $O(n)$.  The chain of deductions is easily verifiable and thus constitutes a proof of unsatisfiability.  In other words, we derive a directed implication graph from the input Horn3SAT formula; the proof of unsatisfiability is then a directed path in the graph from some $x_i$ to $\neg x_i$.

If none of these meets your needs, you'll need to define what you're looking for more carefully.