On proof theory in computer science

TL;DR

This paper discusses how advanced proof theoretic techniques, specifically proof compression, have been used to establish the equality of complexity classes NP, coNP, and PSPACE, resolving longstanding open problems.

Contribution

It presents proof theoretic tree-to-dag compression methods that proved NP = coNP = PSPACE, a significant breakthrough in computational complexity.

Findings

Proved NP = coNP = PSPACE using proof compression techniques.

Established the effectiveness of proof theoretic methods in solving complexity class problems.

Provided new insights into the relationship between proof theory and computational complexity.

Abstract

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)