Here you can download and read the last version of our article reporting our proof that . It was submitted to a specialized journal on Theory of Computation and Computational Complexity. While the referees do not finish their reviewing we decide to provide public access to the text and additional material that do not fit in the format of a journal paper.

The article is here NP vs PSPACE. Besides the proof of the main result, it contains two examples of huge (exponentially big) proofs that are converted to polynomially bounded proofs by means of our compressing method that convert tree-like proofs in dag-like ones. A third example, exponential normal proofs of the Pigeonhole Principle are compressed in polynomially sized dag-like proofs are shown here pdf, written in A3 paper format.

If you want a quicker understanding of the approach used in the proof, please read it here.

You are welcome to criticize the text. Send messages to hermann@inf.puc-rio.br and/or leo.gordeev@gmail.com

Some observations:

As contains , the conjecture is a corollary of ;

Our proof is """constructive""" in the sense it can ""effectively provide polynomial certificates for and complete problems"". It is involving to produce any of these certificates in particular. However, below it is the main steps to follow, if you want to convince yourself about this, after reading the article above. Let us, see why this happen. We consider, firstly a CoNP-complete problem as Non-Hamiltonian graphs (NH). Consider Hamiltonian the problem of knowing that a graph has a hamiltonian path. The steps below provide a polynomial certificate for each non-hamiltonian graph that it is in NH.

Choose your favorite reduction from Hamiltonian to SAT. The chosen reduction provides you with a formula that is satisfiable, iff, has a hamiltonian path, for any graph .

Observe that does not have a hamiltonian path, iff, is not in SAT, iff, is a Classical tautology. We know by Glyvenko theorem, is an Intuitionistic tautology.

Apply the translation cited in our article (a variant of Statman translation) to , producing a purely implicational formula . This formula is of cubic complexity (length) regarded to , and is of polynomial complexity regard to the size of the graph.

Observe, that the translation is a purely implicational minimal (Johansson's logic) tautology, iff, is an intuitionistic tautology.

Prove in the Natural Deduction system for the purely implicational minimal logic, obtaining a proof .

If is polynomially bounded regarded to its conclusion, so it is regarded to the size of the graph. In this case it is a polynomial certificate that is non-hamiltonian.

(THE CRUCIAL CASE) If is of super-polynomial size regarded to lenght, apply the Horizontal Compression described in the above article to in order to obtain a dag-like polynomial proof of the that is polynomially verifiable (see the article) in time. provides a reason why the graph has no hamiltonian path, and it is a certificate (polynomial of course) that belongs to the set of non-hamiltonian graphs.

In order to provide polynomial certificates for -complete problems, it is enough to use your favorite reduction from any -complete problem to Intuitionistic validity (tautology). This can be found in Svejdar's paper for example(see the references in our article). With the formula obtained through this reduction, follow steps 3, 4, 5, 6 and 7 above in order to obtain a polynomial certificate able to be polynomially verifiable in time. Thus, by doing that we can obtain a polynomial certificate for any QBL formula (Quantified Boolean Logic), a quite well-known -complete problem.