{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:13Z","timestamp":1759638973548},"reference-count":69,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":6620,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1995,12]]},"abstract":"<jats:p><jats:bold>\u00a71. Introduction<\/jats:bold>.\n                                                  The classical propositional calculus has an\n                                                  undeserved reputation among logicians as being\n                                                  essentially trivial. I hope to convince the reader\n                                                  that it presents some of the most challenging and\n                                                  intriguing problems in modern logic.<\/jats:p>\n                                                  <jats:p>Although the problem of the complexity of\n                                                  propositional proofs is very natural, it has been\n                                                  investigated systematically only since the late\n                                                  1960s. Interest in the problem arose from two\n                                                  fields connected with computers, automated theorem\n                                                  proving and computational complexity theory. The\n                                                  earliest paper in the subject is a ground-breaking\n                                                  article by Tseitin [62], the published version of\n                                                  a talk given in 1966 at a Leningrad seminar. In\n                                                  the three decades since that talk, substantial\n                                                  progress has been made in determining the relative\n                                                  complexity of proof systems, and in proving strong\n                                                  lower bounds for some restricted proof systems.\n                                                  However, major problems remain to challenge\n                                                  researchers.<\/jats:p>\n                                                  <jats:p>The present paper provides a survey of the\n                                                  field, and of some of the techniques that have\n                                                  proved successful in deriving lower bounds on the\n                                                  complexity of proofs. A major area only touched\n                                                  upon here is the proof theory of bounded\n                                                  arithmetic and its relation to the complexity of\n                                                  propositional proofs. The reader is referred to\n                                                  the book by Buss [10] for background in bounded\n                                                  arithmetic. The forthcoming book by Kraj\u00ed\u010dek [40]\n                                                  also gives a good introduction to bounded\n                                                  arithmetic, as well as covering most of the basic\n                                                  results in complexity of propositional\n                                                  proofs.<\/jats:p>","DOI":"10.2307\/421131","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:08:20Z","timestamp":1146985700000},"page":"425-467","source":"Crossref","is-referenced-by-count":29,"title":["The Complexity of Propositional\n                                                  Proofs"],"prefix":"10.1017","volume":"1","author":[{"given":"Alasdair","family":"Urquhart","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600008027_ref059","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7"},{"key":"S1079898600008027_ref057","volume-title":"Automation of reasoning","author":"Siekmann","year":"1983"},{"key":"S1079898600008027_ref058","first-page":"77","volume-title":"Proceedings of the 19th Annual ACM Symposium on the Theory of Computing","author":"Smolensky","year":"1987"},{"key":"S1079898600008027_ref004","unstructured":"Ajtai Mikl\u00f3s , Symmetric\n                                                  systems of linear equations modulo p, preprint,\n                                                  1993."},{"key":"S1079898600008027_ref068","volume-title":"The complexity of Boolean functions","author":"Wegener","year":"1987"},{"key":"S1079898600008027_ref051","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"S1079898600008027_ref044","first-page":"325","article-title":"Explicit construction of concentrators","volume":"9","author":"Margulis","year":"1973","journal-title":"Problems of Information Transmission"},{"key":"S1079898600008027_ref047","doi-asserted-by":"publisher","DOI":"10.2307\/2269958"},{"key":"S1079898600008027_ref033","volume-title":"Proceedings of the 14th German Workshop on A.I.","volume":"251","author":"Goerdt","year":"1990"},{"key":"S1079898600008027_ref011","doi-asserted-by":"publisher","DOI":"10.2307\/2273826"},{"key":"S1079898600008027_ref043","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19900360106"},{"key":"S1079898600008027_ref039","doi-asserted-by":"publisher","DOI":"10.2307\/2275250"},{"key":"S1079898600008027_ref009","doi-asserted-by":"publisher","DOI":"10.1137\/0221068"},{"key":"S1079898600008027_ref063","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"S1079898600008027_ref062","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"S1079898600008027_ref056","volume-title":"Mathematical logic","author":"Shoenfield","year":"1967"},{"key":"S1079898600008027_ref030","first-page":"364","volume-title":"Proceedings 20th Annual Symposium on Foundations of Computer Science","author":"Gabber","year":"1979"},{"key":"S1079898600008027_ref038","doi-asserted-by":"publisher","DOI":"10.1002\/rsa.3240070103"},{"key":"S1079898600008027_ref064","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90147-3"},{"key":"S1079898600008027_ref037","first-page":"87","volume-title":"Machine intelligence vol. 4","author":"Kowalski","year":"1969"},{"key":"S1079898600008027_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(79)90084-0"},{"key":"S1079898600008027_ref002","first-page":"1","volume-title":"Feasible mathematics","author":"Ajtai","year":"1990"},{"key":"S1079898600008027_ref013","volume-title":"Introduction to mathematical logic","author":"Church","year":"1956"},{"key":"S1079898600008027_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3466-1_3"},{"key":"S1079898600008027_ref008","volume-title":"Annals of Pure and Applied Logic","author":"Beame","year":"1993"},{"key":"S1079898600008027_ref015","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48016"},{"key":"S1079898600008027_ref006","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365714"},{"key":"S1079898600008027_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90044-E"},{"key":"S1079898600008027_ref061","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(78)90011-6"},{"key":"S1079898600008027_ref066","doi-asserted-by":"publisher","DOI":"10.1007\/BF01475439"},{"key":"S1079898600008027_ref060","first-page":"525","volume-title":"Proceedings of the Fourth Hawaii International Symposium on System Sciences","author":"Spira","year":"1971"},{"key":"S1079898600008027_ref032","volume-title":"Computers and intractability. a guide to the theory of NP-completeness","author":"Garey","year":"1979"},{"key":"S1079898600008027_ref052","unstructured":"Reckhow Robert , On the\n                                                  lengths of proofs in the propositional calculus,\n                                                  Ph.D. thesis , University of Toronto,\n                                                  1976."},{"key":"S1079898600008027_ref003","doi-asserted-by":"crossref","unstructured":"Ajtai Mikl\u00f3s , The\n                                                  independence of the modulo p counting principles,\n                                                  preprint, 1993.","DOI":"10.1145\/195058.195207"},{"key":"S1079898600008027_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BF00156916"},{"key":"S1079898600008027_ref045","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/2.2.205"},{"key":"S1079898600008027_ref019","first-page":"15","article-title":"On the lengths of proofs in the propositional calculus","volume":"6","author":"Cook","year":"1974","journal-title":"Proceedings of the Sixth Annual ACM Symposium on the Theory of Computing"},{"key":"S1079898600008027_ref054","first-page":"77","volume-title":"Machine intelligence, vol. 3","author":"Robinson","year":"1968"},{"key":"S1079898600008027_ref035","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"S1079898600008027_ref069","volume-title":"Principia mathematica, vols. 1\u20133","author":"Whitehead","year":"1910"},{"key":"S1079898600008027_ref010","volume-title":"Bounded arithmetic","author":"Buss","year":"1986"},{"key":"S1079898600008027_ref031","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90054-8"},{"key":"S1079898600008027_ref007","first-page":"200","volume-title":"Proceedings of the 24th Annual ACM Symposium on the Theory of Computing","author":"Beame","year":"1992"},{"key":"S1079898600008027_ref042","first-page":"193","volume-title":"Computer science logic (Kaiserlautern, Oct. '89)","author":"Kraj\u00edc\u0306ek","year":"1990"},{"key":"S1079898600008027_ref050","first-page":"598","article-title":"Lower bounds on the size of bounded depth networks over a complete basis with logical addition","volume":"41","author":"Razborov","year":"1987","journal-title":"Matemat. Zametki"},{"key":"S1079898600008027_ref067","doi-asserted-by":"publisher","DOI":"10.1147\/rd.41.0002"},{"key":"S1079898600008027_ref065","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531026"},{"key":"S1079898600008027_ref046","volume-title":"Computational complexity","author":"Papadimitriou","year":"1994"},{"key":"S1079898600008027_ref029","first-page":"260","volume-title":"Proceedings of the 22nd Annual IEEE Symposium on the Foundations ofComputer Science","author":"Furst","year":"1981"},{"key":"S1079898600008027_ref018","first-page":"83","volume-title":"Proceedings of the Seventh Annual ACM Symposium on the Theory of Computation","author":"Cook","year":"1975"},{"key":"S1079898600008027_ref048","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0075316"},{"key":"S1079898600008027_ref024","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"S1079898600008027_ref028","volume-title":"Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens","author":"Frege","year":"1879"},{"key":"S1079898600008027_ref049","doi-asserted-by":"publisher","DOI":"10.1007\/BF01200117"},{"key":"S1079898600008027_ref020","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"S1079898600008027_ref026","unstructured":"Dowd Martin ,\n                                                  Model-theoretic aspects of , unpublished MS,\n                                                  1985."},{"key":"S1079898600008027_ref034","volume-title":"Computational limitations of small-depth circuits","author":"H\u00e5stad","year":"1987"},{"key":"S1079898600008027_ref027","volume-title":"The complexity of Boolean networks","author":"Dunne","year":"1988"},{"key":"S1079898600008027_ref016","first-page":"151","volume-title":"Proceedings of the Third Annual ACM Symposium on the Theory of Computation","author":"Cook","year":"1971"},{"key":"S1079898600008027_ref001","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1109\/SFCS.1988.21951","article-title":"The complexity of the pigeonhole principle","author":"Ajtai","year":"1988","journal-title":"Proceedings of the 29th Annual IEEE Symposium on the Foundations of Computer Science"},{"key":"S1079898600008027_ref025","unstructured":"Dowd Martin , Propositional\n                                                  representation of arithmetic proofs, Ph.D. thesis,\n                                                  University of Toronto, 1979, Department of\n                                                  Computer Science, Technical Report No.\n                                                  132\/79."},{"key":"S1079898600008027_ref041","doi-asserted-by":"publisher","DOI":"10.2307\/2274765"},{"key":"S1079898600008027_ref053","doi-asserted-by":"crossref","unstructured":"Riis S\u00f8ren , Independence\n                                                  in bounded arithmetic, D. Phil. thesis, Oxford\n                                                  University, 1993.","DOI":"10.7146\/brics.v1i23.21644"},{"key":"S1079898600008027_ref005","unstructured":"Beame Paul , A switching\n                                                  lemma primer, preprint,\n                                                  1993."},{"key":"S1079898600008027_ref017","unstructured":"Cook Stephen A. , An\n                                                  exponential example for analytic tableaux,\n                                                  manuscript, 1973."},{"key":"S1079898600008027_ref036","volume-title":"Introduction to automata theory, languages and computation","author":"Hopcroft","year":"1979"},{"key":"S1079898600008027_ref023","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"S1079898600008027_ref040","volume-title":"Bounded arithmetic, propositional logic and complexity theory","author":"Kraj\u00edc\u0306ek","year":"1996"},{"key":"S1079898600008027_ref055","volume-title":"An algorithm for a machine search of a natural logical deduction in a propositional calculus","author":"Shanin","year":"1965"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600008027","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,23]],"date-time":"2020-06-23T09:05:12Z","timestamp":1592903112000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600008027\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":69,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["S1079898600008027"],"URL":"https:\/\/doi.org\/10.2307\/421131","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}