Interactive Proof for HORN-SAT? Is there a way that a prover can convince a verifier that some HORN-SAT expression is satisfiable?

Of course this might seem silly, since there are linear time algorithms for HORN-SAT. On the other hand, HORN-SAT is P-complete, which means it does not have log-space algorithms unless P=L. Accordingly, restrict the computational abilities of the verifier to L. Now the verifier is very feeble, so the problem is no longer silly.

Another twist on this is whether it can be a zero-knowledge proof.
This http://www.cs.ubc.ca/~condon/papers/ips-survey.pdf
survey by Anne Condon contains many facts about space bounded interactive proof systems.

There are several models, and the main differences are whether you allow private coins for the verifier (IP) or public coins only (AM), and whether you also restrict the verification
time to polynomial (not implied by the space bound alone).

Without the time restriction the answer is yes: IP(log-space) contains EXP
and AM(log-space)=P.

Note that IP(log-space) is most likely larger than standard IP. On the other hand 
IP(log-space, poly-time)=IP=PSPACE.

AM(log-space, poly-time) = P due to 'Delegating Computation: Interactive Proofs for Muggles' by Goldwasser et al., STOC 2008.

Furthermore the paper 'Zero knowledge with log-space verifiers' by Kilian (FOCS 88)
shows how to get a log-space poly-time zero knowledge proof system for everything in IP (with private coins obviously).