Some remarks on lengths of propositional proofs

Archive for Mathematical Logic 34 (6):377-394 (1995)
  Copy   BIBTEX

Abstract

We survey the best known lower bounds on symbols and lines in Frege and extended Frege proofs. We prove that in minimum length sequent calculus proofs, no formula is generated twice or used twice on any single branch of the proof. We prove that the number of distinct subformulas in a minimum length Frege proof is linearly bounded by the number of lines. Depthd Frege proofs ofm lines can be transformed into depthd proofs ofO(m d+1) symbols. We show that renaming Frege proof systems are p-equivalent to extended Frege systems. Some open problems in propositional proof length and in logical flow graphs are discussed

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 74,466

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

The Number of Lines in Frege Proofs with Substitution.Alasdair Urquhart - 1997 - Archive for Mathematical Logic 37 (1):15-19.
Cutting Planes, Connectivity, and Threshold Logic.Samuel R. Buss & Peter Clote - 1996 - Archive for Mathematical Logic 35 (1):33-62.
The Cost of a Cycle is a Square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.
Matrix Identities and the Pigeonhole Principle.Michael Soltys & Alasdair Urquhart - 2004 - Archive for Mathematical Logic 43 (3):351-357.
A Note on Propositional Proof Complexity of Some Ramsey-Type Statements.Jan Krajíček - 2011 - Archive for Mathematical Logic 50 (1-2):245-255.
The Complexity of Propositional Proofs.Nathan Segerlind - 2007 - Bulletin of Symbolic Logic 13 (4):417-481.

Analytics

Added to PP
2013-11-23

Downloads
54 (#216,074)

6 months
1 (#417,474)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Cut-Based Abduction.Marcello D'agostino, Marcelo Finger & Dov Gabbay - 2008 - Logic Journal of the IGPL 16 (6):537-560.
Partially Definable Forcing and Bounded Arithmetic.Albert Atserias & Moritz Müller - 2015 - Archive for Mathematical Logic 54 (1-2):1-33.
The Cost of a Cycle is a Square.A. Carbone - 2002 - Journal of Symbolic Logic 67 (1):35-60.

Add more citations