On proof theory in computational complexity: overview

TL;DR

This paper provides an overview of novel proof-theoretic techniques used to establish the equalities NP = coNP = PSPACE, highlighting the compression methods applied to natural deduction and sequent calculus.

Contribution

It introduces a comprehensive overview of proof-theoretic tree-to-dag compression techniques for propositional minimal logic, leading to significant complexity class equalities.

Findings

Proved NP = coNP = PSPACE using proof compression methods

Developed novel proof-theoretic tree-to-dag techniques

Applied to natural deduction and sequent calculus

Abstract

In [GH1] and [GH2] (see also [GH3]) we presented full proof of the equalities NP = coNP = PSPACE. These results have been obtained by the novel proof theoretic tree-to-dag compressing techniques adapted to Prawitz's Natural Deduction (ND) for propositional minimal logic coupled with the corresponding Hudelmaier's cutfree sequent calculus. In this paper we propose an overview of our proofs.