验证压缩和NP与PSPACE II：附录
Proof Compression and NP Versus PSPACE II: Addendum
摘要：
在[3]中，我们用改进的证明论方法证明了猜想NP = PSPACE，该方法结合了Hudelmaier的最小逻辑无割演算（HSC）[5]和相应的最小Prawitz式自然演绎（ND）[6]中的水平压缩。在本附录中，我们展示了如何证明一个较弱的结果NP = coNP，而不涉及HSC。其基本思想（由于第二作者）是省略完整的最小逻辑和压缩只有\naive“正常树状ND反驳的存在性的哈密尔顿圈在给定的非哈密尔顿图，因为哈密尔顿图问题的NP-完全。因此，不严格地说，NP = coNP的证明可以从我们的NP = PSPACE的证明中通过HSC-消去得到[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）http://dx.doi.org/10.18788/0138-0680.2020.16 [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，《自然演绎：一个证明理论研究》。Almqvist和Wiksell，1965年
英文摘要：
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) http://dx.doi.org/10.18788/0138-0680.2020.16 [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
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
