Proof Compression and NP Versus PSPACE II: Addendum

Authors

  • Lew Gordeev University of Tübingen, Department of Computer Science, Nedlitzer Str. 4a, 14612 Falkensee image/svg+xml
  • E. Hermann Haeusler Pontificia Universidade Católica do Rio de Janeiro – RJ, Department of Informatics, Rua Marques de São Vicente, 224, Gávea, Rio de Janeiro, Brazil image/svg+xml https://orcid.org/0000-0002-4999-7476

DOI:

https://doi.org/10.18778/0138-0680.2022.01

Keywords:

graph theory, natural deduction, computational complexity

Abstract

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.

References

S. Arora, B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press (2009).
Google Scholar DOI: https://doi.org/10.1017/CBO9780511804090

L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica, vol. 107(1) (2019), pp. 55–83, DOI: https://doi.org/10.1007/s11225-017-9773-5
Google Scholar DOI: https://doi.org/10.1007/s11225-017-9773-5

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: https://doi.org/10.18778/0138-0680.2020.16
Google Scholar DOI: https://doi.org/10.18778/0138-0680.2020.16

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
Google Scholar

J. Hudelmaier, An O(nlogn)-space decision procedure for intuitionistic propositional logic, Journal of Logic and Computation, vol. 3 (1993), pp. 1–13, DOI: https://doi.org/10.1093/logcom/3.1.63
Google Scholar DOI: https://doi.org/10.1093/logcom/3.1.63

D. Prawitz, Natural deduction: A proof-theoretical study, Almqvist & Wiksell (1965).
Google Scholar

R. Statman, Intuitionistic propositional logic is polynomial-space complete, Theoretical Computer Science, vol. 9 (1979), pp. 67–72, DOI: https://doi.org/10.1016/0304-3975(79)90006-9
Google Scholar DOI: https://doi.org/10.1016/0304-3975(79)90006-9

Downloads

Published

2022-01-07

How to Cite

Gordeev, L., & Haeusler, E. H. (2022). Proof Compression and NP Versus PSPACE II: Addendum. Bulletin of the Section of Logic, 51(2), 197–205. https://doi.org/10.18778/0138-0680.2022.01

Issue

Section

Research Article

Most read articles by the same author(s)