Proof Compression and NP Versus PSPACE II: Addendum
Bulletin of the Section of Logic, Tome 51 (2022) no. 2, pp. 197-205.

Voir la notice de l'article provenant de la source Library of Science

In our previous work we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier’s cut-free sequent calculus for minimal logic (HSC) with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction (ND). In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea (due to the second author) is to omit full minimal logic and compress only “naive” normal tree-like ND refutations of the existence of Hamiltonian cycles in given non-Hamiltonian graphs, since the Hamiltonian graph problem in NPcomplete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE.
Keywords: graph theory, natural deduction, computational complexity
@article{BSL_2022_51_2_a1,
     author = {Gordeev, Lew and Haeusler, Edward Hermann},
     title = {Proof {Compression} and {NP} {Versus} {PSPACE} {II:} {Addendum}},
     journal = {Bulletin of the Section of Logic},
     pages = {197--205},
     publisher = {mathdoc},
     volume = {51},
     number = {2},
     year = {2022},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a1/}
}
TY  - JOUR
AU  - Gordeev, Lew
AU  - Haeusler, Edward Hermann
TI  - Proof Compression and NP Versus PSPACE II: Addendum
JO  - Bulletin of the Section of Logic
PY  - 2022
SP  - 197
EP  - 205
VL  - 51
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a1/
LA  - en
ID  - BSL_2022_51_2_a1
ER  - 
%0 Journal Article
%A Gordeev, Lew
%A Haeusler, Edward Hermann
%T Proof Compression and NP Versus PSPACE II: Addendum
%J Bulletin of the Section of Logic
%D 2022
%P 197-205
%V 51
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a1/
%G en
%F BSL_2022_51_2_a1
Gordeev, Lew; Haeusler, Edward Hermann. Proof Compression and NP Versus PSPACE II: Addendum. Bulletin of the Section of Logic, Tome 51 (2022) no. 2, pp. 197-205. http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a1/

[1] S. Arora, B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press (2009).

[2] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica, vol. 107(1) (2019), pp. 55–83 | DOI

[3] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE II, Bulletin of the Section of Logic, vol. 49(3) (2020), pp. 213–230 | DOI

[4] E. H. Haeusler, Propositional Logics Complexity and the Sub-Formula Property, [in:] Proceedings of the Tenth International Workshop on Developments in Computational Models DCM (2014), URL: https://arxiv.org/abs/1401.8209v3

[5] J. Hudelmaier, An O(nlogn)-space decision procedure for intuitionistic propositional logic, Journal of Logic and Computation, vol. 3 (1993), pp. 1–13 | DOI

[6] D. Prawitz, Natural deduction: A proof-theoretical study, Almqvist Wiksell (1965).

[7] R. Statman, Intuitionistic propositional logic is polynomial-space complete, Theoretical Computer Science, vol. 9 (1979), pp. 67–72 | DOI