References & Citations
Computer Science > Computational Complexity
Title: Proof Compression and NP Versus PSPACE II: Addendum
(Submitted on 17 Nov 2020 (this version), latest version 20 Nov 2020 (v2))
Abstract: In [3] we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier's cut-free sequent calculus for minimal logic (HSC) [5] with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction (ND) [6]. 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 NP-complete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE [3].
[3] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE II, Bulletin of the Section of Logic (49) (3): 213-230 (2020) this http URL [1907.03858]
[5] J. Hudelmaier, An O (n log n)-space decision procedure for intuitionistic propositional logic, J. Logic Computat. (3): 1-13 (1993)
[6] D. Prawitz, Natural deduction: a proof-theoretical study. Almqvist & Wiksell, 1965
Submission history
From: Lev Gordeev [view email][v1] Tue, 17 Nov 2020 17:39:45 GMT (22kb)
[v2] Fri, 20 Nov 2020 13:18:25 GMT (22kb)
Link back to: arXiv, form interface, contact.