Here you can download and read the last version of our article reporting our proof that PSPACE=NP. 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 P^{2n}_n 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 and/or

Some observations:

  • As PSPACE contains CoNP, the conjecture NP=CoNP is a corollary of PSPACE=NP ;

  • Our proof is """constructive""" in the sense it can ""effectively provide polynomial certificates for CoNP  and PSPACE 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 G that it is in NH.

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

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

    3. Apply the translation cited in our article (a variant of Statman translation) to \neg F_G, producing a purely implicational formula (\neg F_G)^{\star}. This formula is of cubic complexity (length) regarded to F_G, and F_G is of polynomial complexity regard to the size of the graph.

    4. Observe, that the translation (\neg F_G)^{\star} is a purely implicational minimal (Johansson's logic) tautology, iff, \neg F_G is an intuitionistic tautology.

    5. Prove (\neg F_G)^{\star} in the Natural Deduction system for the purely implicational minimal logic, obtaining a proof \Pi.

    6. If \Pi 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 G is non-hamiltonian.

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

  • In order to provide polynomial certificates for PSPACE-complete problems, it is enough to use your favorite reduction from any PSPACE-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 PSPACE-complete problem.

TecMF: NPPSPACE (last edited 2016-10-14 08:17:30 by JeffersonSantos)