{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T10:17:05Z","timestamp":1775470625171,"version":"3.50.1"},"reference-count":10,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2012,3,5]],"date-time":"2012-03-05T00:00:00Z","timestamp":1330905600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2012,6]]},"abstract":"<jats:p>A normalization procedure is given for classical natural deduction with the standard rule of indirect proof applied to arbitrary formulas. For normal derivability and the subformula property, it is sufficient to permute down instances of indirect proof whenever they have been used for concluding a major premiss of an elimination rule. The result applies even to natural deduction for classical modal logic.<\/jats:p>","DOI":"10.1017\/s1755020311000311","type":"journal-article","created":{"date-parts":[[2012,3,5]],"date-time":"2012-03-05T23:29:56Z","timestamp":1330990196000},"page":"205-211","source":"Crossref","is-referenced-by-count":12,"title":["NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION"],"prefix":"10.1017","volume":"5","author":[{"given":"JAN VON","family":"PLATO","sequence":"first","affiliation":[]},{"given":"ANNIKA","family":"SIDERS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2012,3,5]]},"reference":[{"key":"S1755020311000311_ref6","volume-title":"The Structural Complexity of Proofs","author":"Statman","year":"1974"},{"key":"S1755020311000311_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100091"},{"key":"S1755020311000311_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139003513"},{"key":"S1755020311000311_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020310000195"},{"key":"S1755020311000311_ref8","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200410054"},{"key":"S1755020311000311_ref4","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"Prawitz","year":"1965"},{"key":"S1755020311000311_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340"},{"key":"S1755020311000311_ref1","doi-asserted-by":"publisher","DOI":"10.21099\/tkbjm\/1496162804"},{"key":"S1755020311000311_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2274910"},{"key":"S1755020311000311_ref10","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1344861886"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020311000311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T21:13:24Z","timestamp":1556226804000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020311000311\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,5]]},"references-count":10,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["S1755020311000311"],"URL":"https:\/\/doi.org\/10.1017\/s1755020311000311","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,5]]}}}