Every super-polynomial proof in purely implicational minimal logic has a polynomially sized proof in classical implicational propositional logic

2015/05/25 by Haeusler, Edward Hermann
#Computational Complexity (cs.CC) #F.2.2 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1505.06506

Abstract

In this article we show how any formula A with a proof in minimal implicational logic that is super-polynomially sized has a polynomially-sized proof in classical implicational propositional logic . This fact provides an argument in favor that any classical propositional tautology has short proofs, i.e., NP=CoNP.

Related

• A Closer Look at Some Recent Proof Compression-Related Claims
• Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic
• Yet another argument in favour of NP=CoNP
• Characterizing Propositional Proofs as Non-Commutative Formulas
• On the Intrinsic Redundancy in Huge Natural Deduction proofs II: Analysing M_\imply Super-Polynomial Proofs