{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T07:40:36Z","timestamp":1707032436859},"reference-count":17,"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":7589,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1993,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce new proof systems for propositional logic,<jats:italic>simple deduction Frege systems, general deduction Frege systems<\/jats:italic>, and<jats:italic>nested deduction Frege systems<\/jats:italic>, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof.<\/jats:p><jats:p>A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by \u201cnearly linear\u201d is meant the ratio of proof lengths is<jats:italic>O<\/jats:italic>(\u03b1(<jats:italic>n<\/jats:italic>)) where \u03b1 is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by<jats:italic>O<\/jats:italic>(<jats:italic>n<\/jats:italic>. \u03b1(<jats:italic>n<\/jats:italic>)). Also we show that a Frege proof of<jats:italic>n<\/jats:italic>lines can be transformed into a tree-like Frege proof of<jats:italic>O<\/jats:italic>(<jats:italic>n<\/jats:italic>log<jats:italic>n<\/jats:italic>) lines and of height<jats:italic>O<\/jats:italic>(log<jats:italic>n<\/jats:italic>). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by<jats:italic>O<\/jats:italic>(<jats:italic>n<\/jats:italic>log<jats:italic>n<\/jats:italic>).<\/jats:p>","DOI":"10.2307\/2275228","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:48:26Z","timestamp":1146955706000},"page":"688-709","source":"Crossref","is-referenced-by-count":15,"title":["The deduction rule and linear and near-linear proof simulations"],"prefix":"10.1017","volume":"58","author":[{"given":"Maria Luisa","family":"Bonet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel R.","family":"Buss","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200021411_ref010","first-page":"87","article-title":"Upper bound on the lengthening of proofs by cut elimination","volume":"137","author":"Orevkov","year":"1984","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova Akademii Nauk SSSR (LOMI)"},{"key":"S0022481200021411_ref003","unstructured":"Bonet M. L. and Buss S. R. , On the serial transitive closure problem (submitted)."},{"key":"S0022481200021411_ref002","unstructured":"Bonet M. L. , The lengths of propositional proofs and the deduction rule, Ph.D. Thesis , U. C. Berkeley, Berkeley, California, 1991."},{"key":"S0022481200021411_ref001","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1093\/oso\/9780198536901.003.0004","volume-title":"Arithmetic, proof theory and computation complexity","author":"Bonet","year":"1993"},{"key":"S0022481200021411_ref016","volume-title":"The collected papers of Gerhard Gentzen","author":"Szabo","year":"1969"},{"key":"S0022481200021411_ref017","volume-title":"Proof theory","author":"Takeuti","year":"1987"},{"key":"S0022481200021411_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"S0022481200021411_ref015","first-page":"505","volume-title":"Logic Colloquium '76","author":"Statman","year":"1977"},{"key":"S0022481200021411_ref008","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1971"},{"key":"S0022481200021411_ref004","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151653"},{"key":"S0022481200021411_ref006","first-page":"83","volume-title":"Proceedings of the 7th annual ACM symposium on theory of computing, 1975","author":"Cook"},{"key":"S0022481200021411_ref007","first-page":"36","volume":"44","author":"Cook","year":"1979","journal-title":"The relative efficiency of propositional proof systems"},{"key":"S0022481200021411_ref005","unstructured":"Buss S. R. , Bounded arithmetic, Bibliopolis , Naples, 1986 (revision of 1985 Ph.D. Thesis , Princeton University, Princeton)."},{"key":"S0022481200021411_ref014","unstructured":"Reckhow R. A. , On the lengths of proofs in the propositional calculus, Ph.D. Thesis , Department of Computer Science, University of Toronto, Toronto, 1976 (technical report #87)."},{"key":"S0022481200021411_ref012","volume-title":"Computational Complexity","author":"Pitassi"},{"key":"S0022481200021411_ref009","unstructured":"Kraj\u00ed\u010dek J. , Lower bounds to the size of constant-depth Frege proofs, this Journal, (to appear)."},{"key":"S0022481200021411_ref011","first-page":"313","article-title":"Reconstruction of a proof from its scheme","volume":"293","author":"Orevkov","year":"1987","journal-title":"Doklady Akademii Nauk SSSR"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200021411","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T07:27:50Z","timestamp":1707031670000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200021411\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,6]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,6]]}},"alternative-id":["S0022481200021411"],"URL":"https:\/\/doi.org\/10.2307\/2275228","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,6]]}}}