-
Proofs of Equalities NP = coNP = PSPACE: Simplification
Authors:
Lev Gordeev,
Edward Hermann Haeusler
Abstract:
In this paper we present simplified proofs of our results NP = coNP = PSPACE.
In this paper we present simplified proofs of our results NP = coNP = PSPACE.
△ Less
Submitted 28 November, 2023;
originally announced November 2023.
-
On proof theory in computational complexity: overview
Authors:
L. Gordeev,
E. H. Haeusler
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.
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.
△ Less
Submitted 9 January, 2022;
originally announced January 2022.
-
On proof theory in computer science
Authors:
L. Gordeev,
E. H. Haeusler
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 relationship…
▽ More
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)
△ Less
Submitted 4 December, 2020;
originally announced December 2020.
-
Proof Compression and NP Versus PSPACE II: Addendum
Authors:
L. Gordeev,
E. H. Haeusler
Abstract:
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)…
▽ More
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
△ Less
Submitted 20 November, 2020; v1 submitted 17 November, 2020;
originally announced November 2020.
-
On P Versus NP
Authors:
Lev Gordeev
Abstract:
Consider a following NP-problem DOUBLE CLIQUE (abbr.: CLIQ$_{2}$): Given a natural number $k>2$ and a pair of two disjoint subgraphs of a fixed graph $G$ decide whether each subgraph in question contains a $k$-clique. I prove that CLIQ$_{2}$ can't be solved in polynomial time by a deterministic TM, which infers $\mathbf{P}\neq \mathbf{NP}$. This proof upgrades the well-known proof of polynomial un…
▽ More
Consider a following NP-problem DOUBLE CLIQUE (abbr.: CLIQ$_{2}$): Given a natural number $k>2$ and a pair of two disjoint subgraphs of a fixed graph $G$ decide whether each subgraph in question contains a $k$-clique. I prove that CLIQ$_{2}$ can't be solved in polynomial time by a deterministic TM, which infers $\mathbf{P}\neq \mathbf{NP}$. This proof upgrades the well-known proof of polynomial unsolvability of the partial result with respect to analogous monotone problem CLIQUE (abbr.: CLIQ) as well as my previous presentation that used appropriate 3-value semantics. Note that problem CLIQ$_{2}$ is not monotone and appears more complex than just iterated CLIQ, as the required subgraphs are mutually dependent.
△ Less
Submitted 14 February, 2024; v1 submitted 2 May, 2020;
originally announced May 2020.
-
Proof compression and NP versus PSPACE. Part 2
Authors:
Lev Gordeev
Abstract:
We upgrade [1] to a complete proof of the conjecture NP = PSPACE.
[1]: L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica (107) (1): 55-83 (2019)
We upgrade [1] to a complete proof of the conjecture NP = PSPACE.
[1]: L. Gordeev, E. H. Haeusler, Proof Compression and NP Versus PSPACE, Studia Logica (107) (1): 55-83 (2019)
△ Less
Submitted 24 July, 2019; v1 submitted 8 July, 2019;
originally announced July 2019.
-
Predicative proof theory of PDL and basic applications
Authors:
Lev Gordeev
Abstract:
Propositional dynamic logic (PDL) is presented in Schütte-style mode as one-sided semiformal tree-like sequent calculus Seq$_ω^{\text{pdl}}$ with standard cut rule and the omega-rule with principal formulas $\left[ P^{\ast }\right] \!A$. The omega-rule-free derivations in Seq$_{ω}^{\text{pdl}}$ are finite (trees) and sequents deducible by these finite derivations are valid in PDL. Moreover the cut…
▽ More
Propositional dynamic logic (PDL) is presented in Schütte-style mode as one-sided semiformal tree-like sequent calculus Seq$_ω^{\text{pdl}}$ with standard cut rule and the omega-rule with principal formulas $\left[ P^{\ast }\right] \!A$. The omega-rule-free derivations in Seq$_{ω}^{\text{pdl}}$ are finite (trees) and sequents deducible by these finite derivations are valid in PDL. Moreover the cut-elimination theorem for Seq$_ω^{\text{pdl}}$ is provable in Peano Arithmetic (PA)extended by transfinite induction up to Veblen's ordinal $\varphi_ω\left( 0\right) $. Hence (by the cutfree subformula property) such predicative extension of PA proves that any given $\left[ P^{\ast }\right] $-free sequent is valid in PDL iff it is deducible in Seq$_ω^{\text{pdl}}$ by a finite cut- and omega-rule-free derivation, while PDL-validity of arbitrary star-free sequents is decidable in polynomial space. The former also implies standard Herbrand-style conclusions, which eventually leads to PSPACE-decidability of PDL-validity of $S$, provided that $P$ is atomic and $A$ is in a suitable \emph{basic conjunctive normal form}. Furthermore we consider star-free formulas $A$ in dual \emph{basic disjunctive normal form}, and corresponding expansions $S=\left\langle P^{\ast }\right\rangle \!A\vee Z$ whose PDL-validity problem is known to be EXPTIME-complete. We show that cutfree-derivability in Seq$_ω^{\text{pdl}}$ (hence PDL-validity) of such $S$\ is equivalent to plain validity of a suitable "transparent" quantified boolean formula $\widehat{S}$. The whole proof can be formalized in PA extended by transfinite induction along $\varphi_ω\left( 0\right)$ -- actually in the corresponding primitive recursive weakening, $\mathbf{PRA}_{\varphi_{ω}\left( 0\right)}$.
△ Less
Submitted 23 February, 2021; v1 submitted 3 April, 2019;
originally announced April 2019.
-
NP vs PSPACE
Authors:
Lew Gordeev,
Edward Hermann Haeusler
Abstract:
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 d…
▽ More
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.
△ Less
Submitted 29 September, 2016;
originally announced September 2016.
-
Proof-graphs for Minimal Implicational Logic
Authors:
Marcela Quispe-Cruz,
Edward Hermann Haeusler,
Lew Gordeev
Abstract:
It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. The aim of this work is to study how to reduce the weight of propositional deductions. We present the formalism of proof-graphs for purely implicational logic, which are graphs of a speci…
▽ More
It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. The aim of this work is to study how to reduce the weight of propositional deductions. We present the formalism of proof-graphs for purely implicational logic, which are graphs of a specific shape that are intended to capture the logical structure of a deduction. The advantage of this formalism is that formulas can be shared in the reduced proof.
In the present paper we give a precise definition of proof-graphs for the minimal implicational logic, together with a normalization procedure for these proof-graphs. In contrast to standard tree-like formalisms, our normalization does not increase the number of nodes, when applied to the corresponding minimal proof-graph representations.
△ Less
Submitted 31 March, 2014;
originally announced April 2014.
