# 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.

• In the non-zero-knowledge case, I think that the naive verification using a satisfying truth assignment as a certificate requires only log space, provided that the input and the certificate are written on read-only tapes which do not count as space. Feb 17 '11 at 6:50
• @Tsuyoshi: I don't see how to do naive verification in only log-space. If we could, wouldn't that show HORN-SAT is in NL, and thus by P-completeness give P = NL? Feb 17 '11 at 17:46
• No. I assumed the certificate is on a read-only tape, which is different from verification performed by NL. Feb 17 '11 at 17:57
• @Tsuyoshi: Ah, so you can read the certificate many times, whereas a certificate-based definition of NL would have a certificate which can only be read once. Feb 18 '11 at 2:37

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).

• I've also found a paper entitled Delegating Computation: Interactive Proofs for Muggles. Does Theorem 3 of this work show that AM(log-space, poly-time) = P? Feb 18 '11 at 2:47
• Yes,they indeed show that! Feb 18 '11 at 11:18