English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

A previous article shows that any linear height bounded normal proof of atautology in the Natural Deduction for Minimal implicational logic$M_{\supset}$ is as huge as it is redundant. More precisely, any proof in afamily of super-polynomially sized and linearly height bounded proofs have asub-derivation that occurs super-polynomially many times in it. In thisarticle, we show that by collapsing all the repeated sub-derivations we obtaina smaller structure, a rooted Directed Acyclic Graph (r-DAG), that ispolynomially 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 otherwords, for every huge proof of a tautology in $M_{\supset}$, we obtain asuccinct certificate for its validity. Moreover, we show an algorithm able tocheck this validity in polynomial time on the certificate's size. Comments onhow the results in this article are related to a proof of the conjecture$NP=CoNP$ appears in conclusion.

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