{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T06:50:32Z","timestamp":1648882232419},"reference-count":15,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4394,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2002,3]]},"abstract":"Abstract<\/jats:title>The present report is a, somewhat lengthy, addendum to [4], where the elimination of cuts from derivations in sequent calculus for classical logic was studied \u2018from the point of view of linear logic\u2019. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative<\/jats:italic> and additive<\/jats:italic> versions of the binary connectives.<\/jats:p>The main novelty here is the observation that this type-distinction<\/jats:italic> is not essential: we can allow classical sequent derivations to use any<\/jats:italic> combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq<\/jats:italic>-reductions.<\/jats:p>We give a detailed description of the simulation of tq<\/jats:italic>-reductions by means of reductions of the interpretation of any given classical proof as a proof net of PN2<\/jats:bold> (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one<\/jats:italic> type, e.g., multiplicative.<\/jats:p>We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent<\/jats:italic>: it is not possible to simulate them internally<\/jats:italic>, i.e.. by only one<\/jats:italic> specific combination, and structural rules.<\/jats:p>","DOI":"10.2178\/jsl\/1190150036","type":"journal-article","created":{"date-parts":[[2007,12,13]],"date-time":"2007-12-13T19:12:10Z","timestamp":1197573130000},"page":"162-196","source":"Crossref","is-referenced-by-count":1,"title":["SN and CR for free-style LKtq<\/sup><\/i>: linear decorations and simulation of normalization"],"prefix":"10.1017","volume":"67","author":[{"given":"Jean-Baptiste","family":"Joinet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harold","family":"Schellinx","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lorenzo Tortora","family":"De Falco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200009919_ref014","volume-title":"Theoretical Computer Science","author":"de Falco","year":"2000"},{"key":"S0022481200009919_ref008","volume-title":"Nuoviproblemi delta logica e della filosofia della scienza, volume II","author":"Girard","year":"1990"},{"key":"S0022481200009919_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0022481200009919_ref001","unstructured":"Danos V. , La logique Lin\u00e9aire appliqu\u00e9e \u00e0 l'\u00e9tude de divers processus de normalisation (principalement du \u03bb-calcul), Ph.D. thesis , Universit\u00e9 Paris VII, 06 1990."},{"key":"S0022481200009919_ref005","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000451"},{"key":"S0022481200009919_ref012","unstructured":"R\u00e9gnier L. , \u03bb-Calculet r\u00e9seaux, Ph.D. thesis , Universit\u00e9 Paris VII, 1992."},{"key":"S0022481200009919_ref004","first-page":"755","volume":"62","author":"Danos","year":"1997","journal-title":"A new deconstructive logic: linear logic"},{"key":"S0022481200009919_ref013","volume-title":"The noble art of linear decorating","author":"Schellinx","year":"1994"},{"key":"S0022481200009919_ref015","unstructured":"de Falco L. Tortora , R\u00e9seaux, coh\u00e9rence et exp\u00e9riences obsessionnelles, Ph.D. thesis , Universit\u00e9 Paris VII, 01 2000."},{"key":"S0022481200009919_ref003","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.011"},{"key":"S0022481200009919_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022564"},{"key":"S0022481200009919_ref010","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61208-4_15"},{"key":"S0022481200009919_ref009","unstructured":"Joinet J.-B. , Etude de la normalisation du calcul des s\u00e9quents classique \u00e0 travers la logique lin\u00e9aire, Ph.D. thesis , Universit\u00e9 Paris VII, January 1993."},{"key":"S0022481200009919_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S0022481200009919_ref011","first-page":"109","volume-title":"Proceedings of the second Scandinavian logic colloquium","author":"Kreisel"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200009919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T01:35:00Z","timestamp":1557192900000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200009919\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0022481200009919"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1190150036","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}