NP与PSPACE
NP vs PSPACE
摘要：
本文证明了猜想$\mathcal{NP}$ = $\mathcal{PSPACE}$，证明了Johansson最小命题逻辑的任意重言式在Prawitz最小命题逻辑系统中允许“小”多项式大小的dag-like自然演绎.这些“小”的扣除产生于标准的“大”\树状输入，通过水平的dag-like压缩，通过合并不同的节点，这些节点标记有在所涉及的扣除的水平部分中出现的相同公式。潜在的“几何”思想：如果高度$h\left( \partial \right) $和不同公式的总数$ϕ\left( \partial \right) $，一个最小重言式$ρ$的给定树状演绎$\partial$都是$ρ$，$\left| ρ\right|$长度的多项式，那么水平dag状压缩的大小至多是$h\left( \partial \right) \times ϕ\left( \partial \right) $，因此是$\left| ρ\right|$的多项式。所附的证明是由于第一作者，但它是第二作者谁提出了一个初步的想法，攻击一个较弱的猜想$\mathcal{NP}= \mathcal{\mathit{co}NP}$减少不同的自然演绎形式主义命题逻辑。这个想法包括交互式使用最小的，直观的和经典的形式主义，所以它的实际实现太复杂了。所附的$ \mathcal{NP}=\mathcal{PSPACE}$的证明运行在最小逻辑的Hudelmaier的无割演算的自然演绎解释之内。
英文摘要：
We present a proof of the conjecture $\mathcal{NP}$ = $\mathcal{PSPACE}$ by showing that arbitrary tautologies of Johansson's minimal propositional logic admit "small" polynomial-size dag-like natural deductions in Prawitz's system for minimal propositional logic. These "small" deductions arise from standard "large"\ tree-like inputs by horizontal dag-like compression that is obtained by merging distinct nodes labeled with identical formulas occurring in horizontal sections of deductions involved. The underlying "geometric" idea: if the height, $h\left( \partial \right) $ , and the total number of distinct formulas, $ϕ\left( \partial \right) $ , of a given tree-like deduction $\partial$ of a minimal tautology $ρ$ are both polynomial in the length of $ρ$, $\left| ρ\right|$, then the size of the horizontal dag-like compression is at most $h\left( \partial \right) \times ϕ\left( \partial \right) $, and hence polynomial in $\left| ρ\right|$. The attached proof is due to the first author, but it was the second author who proposed an initial idea to attack a weaker conjecture $\mathcal{NP}= \mathcal{\mathit{co}NP}$ by reductions in diverse natural deduction formalisms for propositional logic. That idea included interactive use of minimal, intuitionistic and classical formalisms, so its practical implementation was too involved. The attached proof of $ \mathcal{NP}=\mathcal{PSPACE}$ runs inside the natural deduction interpretation of Hudelmaier's cutfree sequent calculus for minimal logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
