-1
$\begingroup$

For the definition of a propositional proof system we have:

An abstract proof system is a polynomial time function f whose range is equal to the set of tautologies. If τ is a tautology, then an f-proof of τ is any value π such that f(π)=τ.

In regards to a polynomially-bounded propositional proof system, we have:

If τ is a tautology, then an f-proof of τ is any value π such that f(π)=τ and |π| $ \leq $ f(τ).

My question is in regards to a regular propositional proof system, does the function need to run in polynomial-time relative to any particular value? What is the polynomial in terms of?

Am I understanding it right, that the polynomial can in fact be in terms of any number, whereas a polynomial-bounded proof system would have the polynomial be in terms of the value of the size of the given tautology?

$\endgroup$
  • $\begingroup$ Could you explain "if we have a proof verifier algorithm Q that does not run in polynomial time we can define a new proof verifier algorithm Q′ which accepts the accenting computations of that verifier Q on a given input π as proofs" a bit more, please? Or do you have any reading suggestions corresponding to that statement? $\endgroup$ – user37484 Feb 9 '16 at 7:50
  • $\begingroup$ Think about Q as a Turing machine. It is straight forward to design a new Turing machine that given strings $\pi$ and $\pi'$ checks if $\pi'$ encodes a computation of Turing machine $Q$ on the input $\pi$ and halts and accepts. That is your $Q'$. In other words, a $Q'$-proof is simply an accepting computation of $Q$. $\endgroup$ – Kaveh Feb 9 '16 at 10:09
4
$\begingroup$

In Cook-Reckhow propositional proof systems proof checkers have to run in polynomial time w.r.t. the size of their input. The size of the input is the size of the proof.

This is generally not a restriction: if we have a proof verifier algorithm $Q$ that does not run in polynomial time we can define a new proof verifier algorithm $Q'$ which accepts the accenting computations of that verifier $Q$ on a given input $\pi$ as proofs. The verifier $Q'$ is computable in polynomial time. The trade-off is that the proof in $Q'$ can be much larger than those in $Q$. E.g. if $Q$ was an exponential time algorithm and $\pi$ was a $Q$-proof for $\varphi$ then there is a $\pi'$ which is a $Q'$ proof for $\varphi$ which consists of the computation of $Q$ on $\pi$. Since the running of $Q$ is exponential the size of $\pi'$ is bounded by an exponential in the size of the original proof $\pi$.

Note that without a restriction on the running time of the verifier the definition is not that useful: TAUT is in coNP and therefore has an exponential time deterministic algorithm which can directly check if a given propositional formula is a tautology.

The existence of a polynomially-bounded proof system is equivalent to the existence of an NP algorithm for TAUT and therefore to NP=coNP.

Also note that in typical proof systems like those based on sequent calculus the proven formula is part of the proof so the size of the proof is an upper bound on the size of the proven formula.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.