{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:11:15Z","timestamp":1767928275363,"version":"3.49.0"},"reference-count":45,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":6036,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1997,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The main concern of this paper is the design of a noetherian and confluent normalization for <jats:bold>LK<\/jats:bold><jats:sup>2<\/jats:sup> (that is, classical second order predicate logic presented as a sequent calculus).<\/jats:p><jats:p>The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's <jats:bold>LC<\/jats:bold> and Parigot's <jats:italic>\u03bb\u03bc<\/jats:italic>, <jats:bold>FD<\/jats:bold> ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine\/Leivant paradigm of \u2018programming-with-proofs\u2019 ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making.<\/jats:p><jats:p>A comparison of our method to that of embedding <jats:bold>LK<\/jats:bold> into <jats:bold>LJ<\/jats:bold> (intuitionistic sequent calculus) brings to the fore the latter's defects for these \u2018deconstructive purposes\u2019.<\/jats:p>","DOI":"10.2307\/2275572","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T19:01:58Z","timestamp":1146942118000},"page":"755-807","source":"Crossref","is-referenced-by-count":89,"title":["A new deconstructive logic: linear logic"],"prefix":"10.1017","volume":"62","author":[{"given":"Vincent","family":"Danos","sequence":"first","affiliation":[]},{"given":"Jean-Baptiste","family":"Joinet","sequence":"additional","affiliation":[]},{"given":"Harold","family":"Schellinx","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200016029_ref002","unstructured":"Danos V. , La logique lin\u00e9aire appliqu\u00e9e \u00e0 l'\u00e9tude de divers processus de normalisation (principalement du lambda-calcul), Th\u00e8se de Doctorat , Universit\u00e9 de Paris 7, 1990."},{"key":"S0022481200016029_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"S0022481200016029_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022564"},{"key":"S0022481200016029_ref039","unstructured":"Regnier L. , \u03bb-calcul et r\u00e9seaux, Th\u00e8se de Doctorat, Universit\u00e9 de Paris 7, 1992."},{"key":"S0022481200016029_ref004","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.011"},{"key":"S0022481200016029_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"S0022481200016029_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0022481200016029_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"S0022481200016029_ref036","first-page":"39","volume-title":"Logic in computer science","author":"Parigot","year":"1993"},{"key":"S0022481200016029_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BF02390456"},{"key":"S0022481200016029_ref033","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0022481200016029_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BF01352934"},{"key":"S0022481200016029_ref038","first-page":"11","volume-title":"Atti del I congresso Italiano di logica","author":"Prawitz","year":"1981"},{"key":"S0022481200016029_ref035","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022575"},{"key":"S0022481200016029_ref037","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0022481200016029_ref001","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0025"},{"key":"S0022481200016029_ref011","volume-title":"Nuovi problemi delta logica e delta filosofia delta scienza","volume":"II","author":"Girard","year":"1991"},{"key":"S0022481200016029_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90093-S"},{"key":"S0022481200016029_ref006","volume-title":"Mathematical intuitionism","author":"Dragalin","year":"1979"},{"key":"S0022481200016029_ref013","first-page":"47","volume-title":"Principles of programming languages","author":"Griffin","year":"1990"},{"key":"S0022481200016029_ref016","volume-title":"Keeping inconsistencies local","author":"H\u00f6rwein","year":"1992"},{"key":"S0022481200016029_ref018","unstructured":"Joinet J.-B. , Etude de la normalisation du calcul des s\u00e9quents classique \u00e0 travers la logique lin\u00e9aire, Th\u00e8se de Doctorat , Universit\u00e9 de Paris 7, 1993."},{"key":"S0022481200016029_ref019","unstructured":"Joinet J.-B. , Schellinx H. , and de Falco L. Tortora , Strong normalization for free deduction and related formalizations of classical second order logic, manuscript, 199?"},{"key":"S0022481200016029_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61208-4_15"},{"key":"S0022481200016029_ref022","volume-title":"Lambda-calcul, types et mod\u00e8les","author":"Krivine","year":"1990"},{"key":"S0022481200016029_ref023","volume-title":"Lambda-calculus, types and models","author":"Krivine","year":"1993"},{"key":"S0022481200016029_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90081-7"},{"key":"S0022481200016029_ref026","first-page":"149","article-title":"Programming with proofs","volume":"26","author":"Krivine","year":"1990","journal-title":"Journal of Information Processing and Cybernetics EIK"},{"key":"S0022481200016029_ref027","doi-asserted-by":"crossref","unstructured":"Leivant D. , Reasoning about functional programs and complexity classes associated to type disciplines, FOCS 83, pp. 460\u2013469, 1983.","DOI":"10.1109\/SFCS.1983.50"},{"key":"S0022481200016029_ref028","first-page":"96","volume-title":"Logic in computer science","author":"Murthy","year":"1991"},{"key":"S0022481200016029_ref029","first-page":"90","volume-title":"Logic in computer science","author":"Murthy","year":"1992"},{"key":"S0022481200016029_ref032","first-page":"361","volume-title":"Russian conference on logic programming","author":"Parigot","year":"1991"},{"key":"S0022481200016029_ref040","unstructured":"Schellinx H. , The noble art of linear decorating, ILLC Dissertation Series 1994-1 , Institute for Logic, Language and Computation, University of Amsterdam, 1994."},{"key":"S0022481200016029_ref042","doi-asserted-by":"publisher","DOI":"10.1007\/BF00885763"},{"key":"S0022481200016029_ref043","volume-title":"CSLI Lecture Notes 29","author":"Troelstra","year":"1992"},{"key":"S0022481200016029_ref044","volume-title":"Constructivism in mathematics: An introduction","volume":"I","author":"Troelstra","year":"1988"},{"key":"S0022481200016029_ref045","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90184-F"},{"key":"S0022481200016029_ref021","first-page":"241","volume":"16","author":"Kreisel","year":"1951","journal-title":"On the interpretation of non-finitist proofs, I"},{"key":"S0022481200016029_ref041","volume-title":"Handbook of mathematical logic","author":"Schwichtenberg","year":"1977"},{"key":"S0022481200016029_ref031","unstructured":"Parigot M. , Proofs of strong normalization for second order classical natural deduction, manuscript, to appear in this Journal."},{"key":"S0022481200016029_ref034","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90042-E"},{"key":"S0022481200016029_ref014","volume-title":"Das Fegefeuer Theorem (De Purgatorio). Eschatol-ogische Axiomatik zum transorbitalen S\u00fcndenmanagement","author":"Heesterbeek","year":"1992"},{"key":"S0022481200016029_ref030","volume-title":"Mixed logic and storage operators","author":"Nour","year":"1995"},{"key":"S0022481200016029_ref017","first-page":"479","volume-title":"To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism","author":"Howard","year":"1980"},{"key":"S0022481200016029_ref015","unstructured":"Herbelin H. , S\u00e9quents qu'on calcule. De l'interpr\u00e9tation du calcul des s\u00e9quents comme calcul de \u03bb-termes et comme calcul de strat\u00e9gies gagnantes, Th\u00e8se de Doctorat , Universit\u00e9 de Paris 7, 1995."}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200016029","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T16:24:59Z","timestamp":1557591899000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200016029\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,9]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,9]]}},"alternative-id":["S0022481200016029"],"URL":"https:\/\/doi.org\/10.2307\/2275572","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,9]]}}}