5

You understand incorrectly. That is not how logic programming works. The number of consequences typically grows exponentially, or is even infinite. For instance, some consequences of $\forall x \in \mathbb{N} \,.\, \phi(x)$ are $\phi(0)$, $\phi(1)$, $\phi(2)$, $\phi(3)$, $\phi(3 + 2)$, $\phi(x \cdot 2)$, and so on. Generating all consequences is infeasable ...


4

The slide describes a proof system for graph non-isomorphism. This is a way for the prover to convince the verifier that the two graphs are non-isormorphic. The soundness of this proof system derives from the fact that it cannot work if the graphs are isomorphic. If $G_0 \equiv G_1$ then no matter what the prover does, the acceptance probability is only $1/2$...


4

When the modulus is a prime $p$, you can compute quadratic residuosity in polynomial time using the Legendre symbol: $x$ is a quadratic residue mod $p$ iff $(x|p)=1$ or $0$. When the modulus is a prime power $p^\alpha$, then you can do the same: I believe $x$ is a quadratic residue mod $p^\alpha$ iff $(x|p)=1$ or $0$. I believe this can be proven using ...


4

I can see some similarity too, but only in a loose sense; there are also some significant differences. Here's the similarity. Define $H_2(x)$ to be the first $d$ bits of $H(x||D)$. Then you can think of the Bitcoin proof-of-work as being: find $x$ such that $H_2(x)=0$. This is loosely similar to the Goldwasser-Sipser protocol; you could imagine that ...


4

This is of course a consequence of $coNP \subset PH \subset PSPACE = IP$. But it can also be proven directly for UNSAT. The basic idea is reducing the problem to zero-testing a sum over a polynomial in a suitable finite field. It's a bit too technical to repeat neatly here, but I can give you an informal idea of how it is done. Let's consider a formula $\...


3

Goldreich and Oren, in their paper Definitions and properties of zero-knowledge proof systems, show that if the verifier is deterministic then interactive proofs trivialize to RP, whereas if the prover is deterministic then interactive proofs trivialize to BPP. See Section 4 of their paper. Blum, de Santis, Micali and Persiano constructed noninteractive ...


3

I think the usual way of doing this is that you hash each record (with a known cryptographically secure hash) and provide the client with $N$ hash values. The client chooses $k$ out of those hash values and you reply with the corresponding $k$ records. The client can then verify that the hash values match up correctly with the provided records plus whatever ...


3

If $x \in L$ then the probability that $(P,V)(x,r) = 1$ is positive, where $r$ is the randomness involved; the probability is over the choice of $r$. In particular, there is some $r$ such that $(P,V)(x,r) = 1$. In contrast, when $x \notin L$, the probability that $(P,V)(x,r) = 0$. That is, there is no $r$ such that $(P,V)(x,r) = 1$. States differently, ...


2

In Haskell there are more programs than there are Coq proofs because Haskell has general recursion whereas Coq does not. (In fact Coq allows you to extract proofs into Haskell code.) The reason that Coq does not have general recursion is that with it we can "prove" anything, simply by saying "to prove $t$ just make a recursive call to itself": ...


2

Yes. We could have defined MIP to allow an exponential number of provers but that is basically the PCP model which is equivalent to MIP with a polynomial (or just two) provers.


2

The class you described is MA (interactive proofs consisting of one round where the prover, Merlin, sends one meassage to the verifier, Arthur, which then has to decide in probabilistic polynomial time whether to accept or reject). Since $BPP\subseteq \Sigma_2\cap \Pi_2$ it immediately follows that $MA\subseteq \Sigma_2\cap \Pi_2$, which is believed to be a ...


2

As usual with zero-knowledge proofs, this is an interactive proof. A prover is trying to prove that he has a satisfying assignment to some 3-SAT formula without giving away the assignment. A verifier is trying to build up enough statistical evidence to believe the prover. The proof proceeds as a series of rounds and continues until the verifier is ...


2

There is no relativizing technique to show that $\mathrm{IP}$ is closed under complement. Clearly, $\mathrm{NP}\subseteq\mathrm{IP}$. Fortnow and Sipser gave an oracle relative to which $\mathrm{co}$-$\mathrm{NP}$ does not have interactive proof system. So, you have to study the arithmetization technique that settles down this conjecture (long ago). Are ...


1

All of these classes can be described as consisting of languages accepted by certain Arthur–Merlin games. In these games, Merlin, an unlimited but potentially dishonest party, tries to convince Arthur, a probabilistic Turing machine, that the input $x$ belongs to the language $L$. We ask that if $x \in L$ then some Merlin convinces Arthur with probability at ...


1

At the very core of Zero Knowledge proof systems, lies the fact that proofs are published by asking the party to prove the correctness of its knowledge, via any one of many methods to verify a solution. Since knowing the question in advance allows a party to forge another proof, the only way to get a reliable proof is via asking a random question out of a ...


1

Here is a zero-knowledge protocol for E3SAT, the variant of SAT in which each clause contains exactly three literals. Consider an instance of E3SAT, consisting of variables $x_1,\ldots,x_n$ and clauses $C_1,\ldots,C_m$. Prover chooses a color in $\{1,2,3,4\}$ for each of the following: Variable literals $V(x_i), V(\lnot x_i)$ ($2n$ colors in total). ...


1

Suppose you have a (randomized) verifier $V$ such that, for all $Q,w$, $$\begin{align*} w\in L &\implies \Pr[V\leftrightarrow P\text{ accepts }w]\geq2/3\\ w\notin L &\implies \Pr[V\leftrightarrow Q\text{ accepts }w]= 0. \end{align*}$$ Since $P$ is one possible value of $Q$, it follows that $$w\notin L \implies \Pr[V\leftrightarrow P\text{ accepts }...


1

I've found an answer to the question I've posed. Here are the tactics I've used: begin unfold pw_o, intros, cases a with h1 h2, let h3 : A := x, let h4 : (g_o x y → g_o x z) ∧ (g_o z x → g_o y x) := h2 x, apply (h4.left h1), end I've unfolded pw_o to make the universal quantifier explicit. After I've isolated pw_o y z as a hypothesis, I'...


1

Here's a deterministic zero-knowledge proof of sorts, if there are any logic gaps please let me know!: This zero knowledge proof involves proving you have a solution to three-colouring a map. The common zero knowledge proof for this scenario (Hats & Crayons for example)involves the Prover tries to convince the Verifier that you have found a solution by ...


1

$AM$ is defined to be $AM[2]$, i.e. languages with 2-rounds Arthur-Merlin protocol, which is equal to $AM[k]$ for any constant $k$. Two extra rounds are required to overcome the fact that the coins are public, i.e. $IP[k]\subseteq AM[k+2]$ for any $k$ , constant or not, as stated in complexity zoo. This means that $IP[poly]=AM[poly]=PSPACE$ (which answers ...


1

To answer the question: No implementation of Haskell to my knowledge has ever represented datatypes as church encodings. I believe that church-style encodings (or variants such as Scott encodings) work equally well for coinductive types.


Only top voted, non community-wiki answers of a minimum length are eligible