{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:48:36Z","timestamp":1781077716900,"version":"3.54.1"},"reference-count":13,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":12795,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1979,3]]},"abstract":"<jats:p>We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.<\/jats:p><jats:p>In \u00a7\u00a72 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In \u00a74 we introduce <jats:italic>extended Frege<\/jats:italic> systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.<\/jats:p>","DOI":"10.2307\/2273702","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:49:34Z","timestamp":1146952174000},"page":"36-50","source":"Crossref","is-referenced-by-count":532,"title":["The relative efficiency of propositional proof systems"],"prefix":"10.1017","volume":"44","author":[{"given":"Stephen A.","family":"Cook","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert A.","family":"Reckhow","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200048702_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/BF01475439"},{"key":"S0022481200048702_ref009","volume-title":"Topics in the theory of computation","author":"Cook","year":"1976"},{"key":"S0022481200048702_ref007","volume-title":"Natural deduction. A proof-theoretic study","author":"Prawitz","year":"1965"},{"key":"S0022481200048702_ref003","first-page":"151","volume-title":"Proceedings of the Third Annual ACM Symposium on the Theory of Computing, May 1971","author":"Cook"},{"key":"S0022481200048702_ref002","unstructured":"Reckhow R. A. , On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976."},{"key":"S0022481200048702_ref001","first-page":"135","volume-title":"Proceedings of the Sixth Annual ACM Symposium on the Theory of Computing, May 1974","author":"Cook"},{"key":"S0022481200048702_ref011","first-page":"83","volume-title":"Proceedings of the Saventh Annual ACM Conference on the Theory of Computing, May 1976","author":"Cook"},{"key":"S0022481200048702_ref005","volume-title":"The design and analysis of computer algorithms","author":"Aho","year":"1974"},{"key":"S0022481200048702_ref012","volume-title":"Introduction to mathematical logic","volume":"I","author":"Church","year":"1956"},{"key":"S0022481200048702_ref006","first-page":"1","volume-title":"From Frege to Godel, a source book in mathematical logic","author":"Frege","year":"1967"},{"key":"S0022481200048702_ref008","first-page":"115","volume-title":"Studies in mathematics and mathematical logic, Part II","author":"Tseitin","year":"1968"},{"key":"S0022481200048702_ref010","volume-title":"Proceedings of Logic Colloquium '76","volume":"87","author":"Statman","year":"1977"},{"key":"S0022481200048702_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200048702","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T21:56:50Z","timestamp":1558907810000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200048702\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979,3]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1979,3]]}},"alternative-id":["S0022481200048702"],"URL":"https:\/\/doi.org\/10.2307\/2273702","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1979,3]]}}}