Sharpened lower bounds for cut elimination

All of RECERCAT

dc.contributor.author	Buss, Samuel R.
dc.contributor.author	Universitat Autònoma de Barcelona. Centre de Recerca Matemàtica
dc.date	2010
dc.identifier	https://ddd.uab.cat/record/76061
dc.identifier	urn:oai:ddd.uab.cat:76061
dc.format	application/pdf
dc.language	eng
dc.publisher	Centre de Recerca Matemàtica
dc.relation	Centre de Recerca Matemàtica. Prepublicacions ;
dc.rights	open access
dc.rights	Aquest document està subjecte a una llicència d'ús de Creative Commons, amb la qual es permet copiar, distribuir i comunicar públicament l'obra sempre que se'n citin l'autor original, la universitat i el centre i no se'n faci cap ús comercial ni obra derivada, tal com queda estipulat en la llicència d'ús
dc.rights	https://creativecommons.org/licenses/by-nc-nd/2.5/
dc.subject	Lògica matemàtica
dc.subject	Demostració, Teoria de la
dc.title	Sharpened lower bounds for cut elimination
dc.type	Article
dc.type	Prepublicació
dc.description.abstract	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 d of the formulas in the original proof. Our new lower bounds remove the constant of proportionality, giving an exponential stack of height equal to d − O(1). The proof method is based on more efficiently expressing the Gentzen-Solovay cut formulas as low depth formulas.