{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,30]],"date-time":"2024-08-30T17:21:42Z","timestamp":1725038502467},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":649,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depth<jats:italic>d<\/jats:italic>of the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal to<jats:italic>d<\/jats:italic>\u2212<jats:italic>O<\/jats:italic>(1). The proof method is based on more efficiently expressing the Gentzen\u2013Solovay cut formulas as low depth formulas.<\/jats:p>","DOI":"10.2178\/jsl\/1333566644","type":"journal-article","created":{"date-parts":[[2012,4,4]],"date-time":"2012-04-04T19:26:53Z","timestamp":1333567613000},"page":"656-668","source":"Crossref","is-referenced-by-count":1,"title":["Sharpened lower bounds for cut elimination"],"prefix":"10.1017","volume":"77","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200000803_ref023","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717"},{"key":"S0022481200000803_ref013","volume-title":"Proof theory and logical complexity","author":"Girard","year":"1987"},{"key":"S0022481200000803_ref018","first-page":"569","volume":"48","author":"Paris","year":"1983","journal-title":"A note on the undefinability of cuts"},{"key":"S0022481200000803_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/BF01095640"},{"key":"S0022481200000803_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF01564760"},{"key":"S0022481200000803_ref014","doi-asserted-by":"publisher","DOI":"10.1515\/9781400858927"},{"key":"S0022481200000803_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90086-H"},{"key":"S0022481200000803_ref003","first-page":"31","volume-title":"Proofs, categories and computations","author":"Baaz","year":"2010"},{"key":"S0022481200000803_ref027","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.042"},{"key":"S0022481200000803_ref017","first-page":"292","article-title":"Applications of cut elimination to obtain estimates of proof lengths","volume":"36","author":"Orevkov","year":"1988","journal-title":"Soviet Mathematics Doklady"},{"key":"S0022481200000803_ref012","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1117755147"},{"key":"S0022481200000803_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062837"},{"key":"S0022481200000803_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.053"},{"key":"S0022481200000803_ref021","first-page":"104","article-title":"Lower bounds on Herbrand's theorem","volume":"75","author":"Statman","year":"1979","journal-title":"Proceedings of the American Mathematical Society"},{"key":"S0022481200000803_ref007","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200910111"},{"key":"S0022481200000803_ref015","doi-asserted-by":"publisher","DOI":"10.1007\/BF01629444"},{"key":"S0022481200000803_ref024","first-page":"1","volume-title":"Intuitionism and proof theory","author":"Yessenin-Volpin","year":"1970"},{"key":"S0022481200000803_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00026-8"},{"key":"S0022481200000803_ref020","unstructured":"Solovay Robert M. , Letter to P. Hajek, 08 1976."},{"key":"S0022481200000803_ref026","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90087-6"},{"key":"S0022481200000803_ref022","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1981-0597664-7"},{"key":"S0022481200000803_ref010","volume-title":"Collected papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S0022481200000803_ref011","first-page":"212","volume-title":"Computer Science Logic 2003","volume":"2803","author":"Gerhardy","year":"2003"},{"key":"S0022481200000803_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(98)80023-2"},{"key":"S0022481200000803_ref001","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","article-title":"On Skolemizations and proof complexity","volume":"20","author":"Baaz","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"S0022481200000803_ref006","unstructured":"Buss Samuel R. , Cut elimination in situ, typeset manuscript, 2011."},{"key":"S0022481200000803_ref005","first-page":"1","volume-title":"Handbook of proof theory","author":"Buss","year":"1998"}],"container-title":["The Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200000803","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,5]],"date-time":"2020-07-05T11:57:22Z","timestamp":1593950242000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200000803\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["S0022481200000803"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1333566644","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6]]}}}