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.