{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T08:05:09Z","timestamp":1758960309195,"version":"3.37.3"},"reference-count":20,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2020,6,17]],"date-time":"2020-06-17T00:00:00Z","timestamp":1592352000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100004564","name":"Ministry of Education, Science and Technological Development of the Republic of Serbia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004564","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9,24]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In derivations of a sequent system, $\\mathcal{L}\\mathcal{J}$, and a natural deduction system, $\\mathcal{N}\\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\\mathcal{N}\\mathcal{J}$ and $\\mathcal{L}\\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\\mathcal{N}\\mathcal{J}$-derivation is normal $\\Longleftrightarrow $ it has the subformula property based on trails $\\Longleftrightarrow $ its $g$-image in $\\mathcal{L}\\mathcal{J}$ is without maximum cuts $\\Longrightarrow $ that $g$-image has the subformula property based on trails. In $\\mathcal{L}\\mathcal{J}$-derivations, another type of cuts, sub-cuts, will be introduced, and it will be proved the following: all cuts of an $\\mathcal{L}\\mathcal{J}$-derivation are sub-cuts $\\Longleftrightarrow $ it has the subformula property based on trails.<\/jats:p>","DOI":"10.1093\/jigpal\/jzaa017","type":"journal-article","created":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T11:09:24Z","timestamp":1586948964000},"page":"739-768","source":"Crossref","is-referenced-by-count":3,"title":["The subformula property of natural deduction derivations and analytic cuts"],"prefix":"10.1093","volume":"29","author":[{"given":"Mirjana","family":"Borisavljevi\u0107","sequence":"first","affiliation":[{"name":"Faculty of Transport and Traffic Engineering, University of Belgrade, Vojvode Stepe 305, 11000 Belgrade, Serbia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2020,6,17]]},"reference":[{"key":"2021091710462195300_ref1","first-page":"40","article-title":"Maximum segments and cuts","volume-title":"Proceedings of the 6th Panhellenic Logic Symposium","author":"Borisavljevi\u0107","year":"2006"},{"key":"2021091710462195300_ref2","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/s10992-008-9084-4","article-title":"Normal derivations and sequent derivations","volume":"37","author":"Borisavljevi\u0107","year":"2008","journal-title":"Journal of Philosophical Logic"},{"key":"2021091710462195300_ref3","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1017\/S1755020318000102","volume":"11","author":"Borisavljevi\u0107","year":"2018","journal-title":"Review of Symbolic Logic"},{"key":"2021091710462195300_ref4","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0168-0072(91)90059-U","article-title":"The undecidability of k-provability","volume":"53","author":"Buss","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"key":"2021091710462195300_ref5","first-page":"733","article-title":"Analytic cut trees","volume-title":"Logic Journal of the IGPL","author":"Cellucci","year":"2000"},{"key":"2021091710462195300_ref6","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/s11225-019-09847-4","article-title":"Normality, non-contamination and logical depth in classical natural deduction","volume":"108","author":"D\u2019Agostino","year":"2020","journal-title":"Studia Logica"},{"key":"2021091710462195300_ref7","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","article-title":"The taming of the cut. Classical refutations with analytic cut","volume":"4","author":"D\u2019agostino","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"2021091710462195300_ref8","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-319-11041-7_7","article-title":"Cut elimination, substitution and normalisation","volume-title":"Dag Prawitz on Proofs and Meaning","author":"Dyckhoff","year":"2015"},{"key":"2021091710462195300_ref9","first-page":"176","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume-title":"Mathematische Zeitschrift","author":"Gentzen","year":"1935"},{"volume-title":"The Collected Papers of Gerhard Gentzen","year":"1969","author":"Gentzen","key":"2021091710462195300_ref10"},{"key":"2021091710462195300_ref11","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1017\/S175502031600040X","article-title":"Analytic cut and interpolation for bi-intuitionistic logic","volume":"10","author":"Kowalski","year":"2017","journal-title":"Review of Symbolic Logic"},{"key":"2021091710462195300_ref12","first-page":"469","volume-title":"Kreiseliana: About and Around Georg Kreisel","author":"Minc","year":"1996"},{"key":"2021091710462195300_ref13","first-page":"240","article-title":"Gentzen\u2019s proof of normalization for natural deduction","volume-title":"The Bulletin of Symbolic Logic","author":"von Plato","year":"2008"},{"key":"2021091710462195300_ref14","first-page":"43","article-title":"A sequent calculus isomorphic to Gentzen\u2019s natural deduction","volume-title":"Review of Symbolic Logic","author":"von Plato","year":"2011"},{"key":"2021091710462195300_ref15","first-page":"323","article-title":"Normalization as a homomorrhic image of cut elimination","volume":"12","author":"Pottinger","year":"1977","journal-title":"Annals of Pure and Applied Logic"},{"volume-title":"Natural Deduction","year":"1965","author":"Prawitz","key":"2021091710462195300_ref16"},{"key":"2021091710462195300_ref17","first-page":"560","article-title":"Analytic cut","volume-title":"Jounal of Symbolic Logic","author":"Smullyan","year":"1969"},{"volume-title":"Basic Proof Theory","year":"1996","author":"Troelstra","key":"2021091710462195300_ref18"},{"key":"2021091710462195300_ref19","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-94-007-7548-0_2","article-title":"Revisiting Zucker\u2019s work on the correspondence between cut-elimination and normalisation","volume-title":"Advances in Natural Deduction, A Celebration of Dag Prawitz\u2019s Work","author":"Urban","year":"2014"},{"key":"2021091710462195300_ref20","first-page":"1","article-title":"The correspondence between cut-elimination and normalization","volume":"7","author":"Zucker","year":"1974","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/5\/739\/40331111\/jzaa017.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/jigpal\/article-pdf\/29\/5\/739\/40331111\/jzaa017.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,29]],"date-time":"2023-09-29T23:27:16Z","timestamp":1696030036000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/29\/5\/739\/5856890"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,17]]},"references-count":20,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2020,6,17]]},"published-print":{"date-parts":[[2021,9,24]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzaa017","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"type":"print","value":"1367-0751"},{"type":"electronic","value":"1368-9894"}],"subject":[],"published-other":{"date-parts":[[2021,10]]},"published":{"date-parts":[[2020,6,17]]}}}