reputation among logicians as being essentially trivial. I hope to convince the reader that it presents some of the most challenging and intriguing problems in modern logic. Although the problem of the complexity of propositional proofs is very natural, it has been investigated systematically only since the late 1960s [Book Review]

Bulletin of Symbolic Logic 1 (4):425-467 (1995)
  Copy   BIBTEX

Abstract

§1. Introduction. The classical propositional calculus has an undeserved reputation among logicians as being essentially trivial. I hope to convince the reader that it presents some of the most challenging and intriguing problems in modern logic. Although the problem of the complexity of propositional proofs is very natural, it has been investigated systematically only since the late 1960s. Interest in the problem arose from two fields connected with computers, automated theorem proving and computational complexity theory. The earliest paper in the subject is a ground-breaking article by Tseitin [62], the published version of a talk given in 1966 at a Leningrad seminar. In the three decades since that talk, substantial progress has been made in determining the relative complexity of proof systems, and in proving strong lower bounds for some restricted proof systems. However, major problems remain to challenge researchers. The present paper provides a survey of the field, and of some of the techniques that have proved successful in deriving lower bounds on the complexity of proofs. A major area only touched upon here is the proof theory of bounded arithmetic and its relation to the complexity of propositional proofs. The reader is referred to the book by Buss [10] for background in bounded arithmetic. The forthcoming book by Krajíček [40] also gives a good introduction to bounded arithmetic, as well as covering most of the basic results in complexity of propositional proofs.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,316

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

Analytics

Added to PP
2014-01-21

Downloads
25 (#742,042)

6 months
4 (#1,172,037)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Alasdair Urquhart
University of Toronto, St. George Campus

Citations of this work

Non-transitive Correspondence Analysis.Yaroslav Petrukhin & Vasily Shangin - 2023 - Journal of Logic, Language and Information 32 (2):247-273.

Add more citations

References found in this work

Introduction to mathematical logic.Alonso Church - 1958 - Revue de Métaphysique et de Morale 63 (1):118-118.
Existence and feasibility in arithmetic.Rohit Parikh - 1971 - Journal of Symbolic Logic 36 (3):494-508.

View all 15 references / Add more references