论计算机科学中的证明论
On proof theory in computer science
摘要：
计算机科学中的主题逻辑应该包含证明理论应用。因此，问题出现了计算复杂性的开放问题是否可以通过先进的证明理论技术来解决。特别地，考虑复杂性类NP、coNP和PSPACE。众所周知，NP和coNP包含在PSPACE中，但直到最近，这些关系的精确表征仍然是开放的。现在[2]，[3]（也见[4]）给出了相应的等式NP = coNP = PSPACE的证明。这些结果是通过适当的证明理论树到dag压缩技术获得的，下面将详细解释。[2]L. Gordeev，E. H. Haeusler，Proof Compression and NP Versus PSPACE，Studia Logica（107）（1）：55{83（2019）[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 [4] L. Gordeev，E. H. Haeusler，证明压缩和NP与PSPACE II：附录，arXiv：2011.09262（2020）
英文摘要：
The subject logic in computer science should entail proof theoretic applications. So the question arises whether open problems in computational complexity can be solved by advanced proof theoretic techniques. In particular, consider the complexity classes NP, coNP and PSPACE. It is well-known that NP and coNP are contained in PSPACE, but till recently precise characterization of these relationships remained open. Now [2], [3] (see also [4]) presented proofs of corresponding equalities NP = coNP = PSPACE. These results were obtained by appropriate proof theoretic tree-to-dag compressing techniques to be briefy explained below. [2] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica (107) (1): 55{83 (2019) [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 [4] L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE II: Addendum, arXiv:2011.09262 (2020)
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
