We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.CC

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Computational Complexity

Title: Going from the huge to the small: Efficient succinct representation of proofs in Minimal implicational logic

Abstract: A previous article shows that any linear height bounded normal proof of a tautology in the Natural Deduction for Minimal implicational logic $M_{\supset}$ is as huge as it is redundant. More precisely, any proof in a family of super-polynomially sized and linearly height bounded proofs have a sub-derivation that occurs super-polynomially many times in it. In this article, we show that by collapsing all the repeated sub-derivations we obtain a smaller structure, a rooted Directed Acyclic Graph (r-DAG), that is polynomially upper-bounded on the size of $\alpha$ and it is a certificate that $\alpha$ is a tautology that can be verified in polynomial time. In other words, for every huge proof of a tautology in $M_{\supset}$, we obtain a succinct certificate for its validity. Moreover, we show an algorithm able to check this validity in polynomial time on the certificate's size. Comments on how the results in this article are related to a proof of the conjecture $NP=CoNP$ appears in conclusion.
Comments: Companion to arXiv:2009.09802v1
Subjects: Computational Complexity (cs.CC); Logic in Computer Science (cs.LO)
Cite as: arXiv:2012.07833 [cs.CC]
  (or arXiv:2012.07833v1 [cs.CC] for this version)

Submission history

From: Edward Haeusler [view email]
[v1] Fri, 11 Dec 2020 21:13:58 GMT (37kb)
[v2] Mon, 25 Jan 2021 15:19:51 GMT (39kb)

Link back to: arXiv, form interface, contact.