Lower Bounds to the size of constant-depth propositional proofs

Journal of Symbolic Logic 59 (1):73-86 (1994)
  Copy   BIBTEX

Abstract

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole principle.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 76,479

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
The cost of a cycle is a square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
Lower Bounds for Modal Logics.Pavel Hrubeš - 2007 - Journal of Symbolic Logic 72 (3):941 - 958.

Analytics

Added to PP
2009-01-28

Downloads
228 (#55,355)

6 months
3 (#228,007)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The complexity of propositional proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.
The complexity of propositional proofs.Alasdair Urquhart - 1995 - Bulletin of Symbolic Logic 1 (4):425-467.
Tautologies from pseudo-random generators.Jan Krajíček - 2001 - Bulletin of Symbolic Logic 7 (2):197-212.

View all 18 citations / Add more citations

References found in this work

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.

Add more references