{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T23:24:11Z","timestamp":1648509851656},"reference-count":8,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4842,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,12]]},"abstract":"<jats:p>In this work we show how some useful reductions known from ordinary intuitionistic propositional calculus can be modified for Intuitionistic Linear Logic (without modalities). The main reductions we consider are: (1) the reduction of the depth of formulas in the sequents by addition of new variables, and (2) the elimination of linear disjunction, tensor and constant F. Both transformations preserve deducibility, that is, a transformed sequent is deducible if and only if the initial one was deducible. The size of the sequent grows linearly in case (1) and \u2264 On<jats:sup>8<\/jats:sup> in case (2).<\/jats:p>","DOI":"10.1017\/s0960129500001201","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:09Z","timestamp":1236157209000},"page":"483-499","source":"Crossref","is-referenced-by-count":2,"title":["Reductions in Intuitionistic Linear Logic"],"prefix":"10.1017","volume":"5","author":[{"given":"Sergei","family":"Soloviev","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500001201_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/BF01069164"},{"key":"S0960129500001201_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(91)90025-W"},{"key":"S0960129500001201_ref001","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0055952-4"},{"key":"S0960129500001201_ref006","unstructured":"Engberg U. and Winskel G. (1992) Petri Nets as Models of Linear Logic."},{"key":"S0960129500001201_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF01629449"},{"key":"S0960129500001201_ref008","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Szabo","year":"1978"},{"key":"S0960129500001201_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014972"},{"key":"S0960129500001201_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BF01703261"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500001201","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T20:12:44Z","timestamp":1557778364000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500001201\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,12]]},"references-count":8,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,12]]}},"alternative-id":["S0960129500001201"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500001201","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,12]]}}}