@article{10.1007/s11225-017-9773-5,
    Abstract = {We show that arbitrary tautologies of Johansson's minimal propositional logic are provable by "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, $$hleft( partial right) $$h , and the total number of distinct formulas, $$phi left( partial right) $$ , of a given tree-like deduction $$partial $$ of a minimal tautology $$rho $$ are both polynomial in the length of $$rho $$ , $$left| rho right| $$ , then the size of the horizontal dag-like compression $$partial ^{{textsc {c}} }$$ C is at most $$hleft( partial right) times phi left( partial right) $$h , and hence polynomial in $$left| rho right| $$ . That minimal tautologies $$ rho $$ are provable by tree-like natural deductions $$partial $$ with $$left| rho right| $$ -polynomial $$hleft( partial right) $$h and $$phi left( partial right) $$ follows via embedding from Hudelmaier's result that there are analogous sequent calculus deductions of sequent $$Rightarrow rho $$ . The notion of dag-like provability involved is more sophisticated than Prawitz's tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic (Savitch in J Comput Syst Sci 4(2):177---192, 1970); Statman in Theor Comput Sci 9(1):67---72, 1979; Svejdar in Arch Math Log 42(7):711---716, 2003).},
    Address = {Berlin, Heidelberg},
    Author = {Gordeev, L. and Haeusler, E. H.},
    File = {Proof Compression and NP Versus PSPACE - Gordeev-Haeusler2019\_Article\_ProofCompressionAndNPVersusPSP - g.pdf},
    ISSN = {0039-3215},
    Journal = {Stud. Log.},
    Keywords = {Propositional complexity, Digraphs, Minimal logic, Proof theory},
    Month = {February},
    Number = {1},
    Pages = {53--83},
    Publisher = {Springer-Verlag},
    Title = {Proof Compression and NP Versus PSPACE},
    URL = {https://doi.org/10.1007/s11225-017-9773-5},
    Volume = {107},
    Year = {2019},
    bdsk-url-1 = {https://doi.org/10.1007/s11225-017-9773-5},
    date-added = {2020-11-19 13:14:28 +0100},
    date-modified = {2020-11-19 13:14:28 +0100},
    issue_date = {February 2019},
    numpages = {31},
    doi = {10.1007/s11225-017-9773-5}
}

@article{10.1007/s11225-017-9773-5, Abstract = {We show that arbitrary tautologies of Johansson's minimal propositional logic are provable by "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, $$hleft( partial right) $$h , and the total number of distinct formulas, $$phi left( partial right) $$ , of a given tree-like deduction $$partial $$ of a minimal tautology $$rho $$ are both polynomial in the length of $$rho $$ , $$left| rho right| $$ , then the size of the horizontal dag-like compression $$partial ^{{textsc {c}} }$$ C is at most $$hleft( partial right) times phi left( partial right) $$h , and hence polynomial in $$left| rho right| $$ . That minimal tautologies $$ rho $$ are provable by tree-like natural deductions $$partial $$ with $$left| rho right| $$ -polynomial $$hleft( partial right) $$h and $$phi left( partial right) $$ follows via embedding from Hudelmaier's result that there are analogous sequent calculus deductions of sequent $$Rightarrow rho $$ . The notion of dag-like provability involved is more sophisticated than Prawitz's tree-like one and its complexity is not clear yet. Our approach nevertheless provides a convergent sequence of NP lower approximations of PSPACE-complete validity of minimal logic (Savitch in J Comput Syst Sci 4(2):177---192, 1970); Statman in Theor Comput Sci 9(1):67---72, 1979; Svejdar in Arch Math Log 42(7):711---716, 2003).}, Address = {Berlin, Heidelberg}, Author = {Gordeev, L. and Haeusler, E. H.}, File = {Proof Compression and NP Versus PSPACE - Gordeev-Haeusler2019_Article_ProofCompressionAndNPVersusPSP - g.pdf}, ISSN = {0039-3215}, Journal = {Stud. Log.}, Keywords = {Propositional complexity, Digraphs, Minimal logic, Proof theory}, Month = {February}, Number = {1}, Pages = {53--83}, Publisher = {Springer-Verlag}, Title = {Proof Compression and NP Versus PSPACE}, URL = {https://doi.org/10.1007/s11225-017-9773-5}, Volume = {107}, Year = {2019}, bdsk-url-1 = {https://doi.org/10.1007/s11225-017-9773-5}, date-added = {2020-11-19 13:14:28 +0100}, date-modified = {2020-11-19 13:14:28 +0100}, issue_date = {February 2019}, numpages = {31}, doi = {10.1007/s11225-017-9773-5} }