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/

Zendy Open

Presents the pdf analysis as premium feature

PDF Analysis

Insights

Presents the summarisation as premium feature

Summarisation

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

In this article we present a class of formulas ϕn,0≤n, that need at least 2n assumption occurrences of other formula βn in any normal proof in Natural Deduction for purely implicational minimal propositional logic (M→). In classical implicational logic, each ϕn have normal proofs using at most one assumption occurrence. As a consequence, normal proofs of ϕn have exponential lower bound in M→ and linear lower bound in its classical version. In fact, 2n is the lower-bound for cut-free Sequent proofs too. The existence of this class of formulas have strong influence in designing automatic proof-procedures based in such systems. It is discussed proof-theoretically how tautologies in purely implicational classical logic can be proved by polynomially sized derivations when their minimal counterpart is exponentially sized

How Many Times do We Need an Assumption to Prove a Tautology in Minimal Logic? Examples on the Compression Power of Classical Reasoning