{"entities":{"Q276260":{"pageid":278027,"ns":120,"title":"Item:Q276260","lastrevid":60717540,"modified":"2026-04-10T18:42:32Z","type":"item","id":"Q276260","labels":{"en":{"language":"en","value":"A semantic account of strong normalization in linear logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6576633"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$9DF86318-6012-47F1-AD39-9DB21BA47AAB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c13b971c5fd12867f85cc76f1ca775eee783b1d7","datavalue":{"value":{"text":"A semantic account of strong normalization in linear logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q276260$57B75086-3DA6-418A-AFD2-A5145C738E57","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"73f072f7582c5fe6b14786a2dae7c585f08c91cc","datavalue":{"value":"1353.03077","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$002D52CE-1A69-4150-A551-83D0BD7397FF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"98d17c34f7570301f50f71cd9e0d89b712b5d33a","datavalue":{"value":{"entity-type":"item","numeric-id":276258,"id":"Q276258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$49799F45-85E2-4F0C-AE07-590551C31D74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ddd92fba6e58ba3ad12b0f7634976998ce8fce29","datavalue":{"value":{"entity-type":"item","numeric-id":276259,"id":"Q276259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$615B6E80-FB06-44E9-928D-581D96C8E3BC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$13F6851D-ECE3-4366-8A33-4AE13EF801C9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e14340917da0b560f1aa784255616bd78a4a4ba6","datavalue":{"value":{"time":"+2016-05-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q276260$163CB5AB-3C07-411A-8989-99D951B052F2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"baab616597831c631bc635396b36daf10b620102","datavalue":{"value":"https://arxiv.org/abs/1304.6762","type":"string"},"datatype":"url"},"type":"statement","id":"Q276260$BE28A584-7C44-4F73-B6F1-3489E7CD86E8","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"15a5be954de63b9a09120e92802adc210813c3df","datavalue":{"value":{"entity-type":"item","numeric-id":424544,"id":"Q424544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$71BC25F3-6DC3-47DB-9A1F-3453E6133686","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$ECAF9211-7184-4D86-AA47-AB77C0DA093F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$094FC88B-E55A-4894-946C-B151B6BB12A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$947F8AC3-DD3D-45CD-9A73-86FF204BA348","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$6E21B17B-51A2-4B6D-9F90-C97FB7585ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cf173b17cb29f39acd7ecc1fdf48aa6cf6900643","datavalue":{"value":"18C50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$506ADC0F-0497-43DE-B532-E776F87E9023","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be373f5fcca324ce519e4c6c152942e62e753b0f","datavalue":{"value":"6576633","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$5AF05E7F-DA9C-44A4-8077-56C87AD0A5B2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$77F69006-9B96-4399-8080-1FDC1F6692C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$23814B51-5871-41A8-BE2B-93EC5EC103D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d82d54321dd9799ec54c6e2eeabcd189cda5e80a","datavalue":{"value":"proof nets","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$8463EA1D-6608-4C65-8166-2CBF6DFA9EAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51802126f63d5102d578f2858428d5d0f09da73b","datavalue":{"value":"denotational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$6A5616BD-C4C4-4F4F-B0FB-628C94C7B7C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ba0cc3f7aaac8445724ef309c9eecb57f5a563d","datavalue":{"value":"computational complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$A75F96A7-85F2-4F02-AF81-83FC2E60F64C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$94B9073D-203D-469C-9294-BA7119E39D64","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$4048AA1C-2576-461C-A8E2-56A359A49ABF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0c7c70d597cb3456426052489044f05b5ee0438b","datavalue":{"value":"W1630373979","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$A71E1CB3-1C61-4F08-BDC7-DFEB4981D5CE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c124b1eef9f41e78cedafbab76b9dfc77596cb59","datavalue":{"value":{"entity-type":"item","numeric-id":2958373,"id":"Q2958373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$EDA52891-3B2D-4CF1-A07B-8545237EEF80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06d3a18112634d945f57a45436f6c38b7d9c07d1","datavalue":{"value":{"entity-type":"item","numeric-id":2851671,"id":"Q2851671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$04941975-9437-4DC2-8419-5ED1B1CCC71C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f524a2f71b178502e011bbad6797a16072654b53","datavalue":{"value":{"entity-type":"item","numeric-id":3000601,"id":"Q3000601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$55915214-B04D-4F30-A1F2-9E44DE3C5F3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e30e94607211c12d1cd576c4053c05edcdb12d9d","datavalue":{"value":{"entity-type":"item","numeric-id":2915673,"id":"Q2915673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$E4FDBF8A-5A79-449B-B40A-4AF63139AAEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"396079bf6c00688a3a618a05bc699938cbbf9c06","datavalue":{"value":{"entity-type":"item","numeric-id":3190172,"id":"Q3190172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$3EB7F4F5-F5A6-4882-9AF7-27542137306A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a15b944588e7daa1d682743e9f423a10e7c94e5","datavalue":{"value":{"entity-type":"item","numeric-id":1134141,"id":"Q1134141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$202498D1-59B8-4E0A-B214-9C7D67B89BFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdb9e1d8ac47b2da5172822d140197006c8b55fe","datavalue":{"value":{"entity-type":"item","numeric-id":4842980,"id":"Q4842980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$C853E995-F171-48DE-BEEA-B7AF9ACE797E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c99fad36f552f6c9f003614420eedba916456aa8","datavalue":{"value":{"entity-type":"item","numeric-id":4577984,"id":"Q4577984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$9EFF2C7A-2940-42EE-9E43-C49531321DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8074052239bebe7f1daac4df3d727319b24d7fe","datavalue":{"value":{"entity-type":"item","numeric-id":5278430,"id":"Q5278430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$F4172970-D876-41A9-B89C-8FCDC54E21BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1245adc65c7a6a43c03977a394ea4c343893ad84","datavalue":{"value":{"entity-type":"item","numeric-id":534698,"id":"Q534698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$43D43099-7EAF-4C77-8B3C-08A321038D75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9096eab74af1d913ef60f62dc9d9e246d39a437","datavalue":{"value":{"entity-type":"item","numeric-id":435194,"id":"Q435194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$888384AF-2303-4E15-B9FB-A8264C5BABE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b27d44a0e50fda314668a36654efb04ab5135cb3","datavalue":{"value":{"entity-type":"item","numeric-id":3868730,"id":"Q3868730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$516A6F9F-91FB-4E47-A7D6-6AADEB296968","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2edb7a0c6ea1f06765b6708ba458501deba3011d","datavalue":{"value":{"entity-type":"item","numeric-id":5898816,"id":"Q5898816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$BBE559CF-13E8-46C6-A18F-7B21FF638805","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44344e1b9d06c74b17ab363ea3c3099e86c02d07","datavalue":{"value":{"entity-type":"item","numeric-id":860836,"id":"Q860836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$C7E1D636-7BAF-46CB-917E-6A98FF9926C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1209cc2519c0798504384b3a297a5def88b5a62","datavalue":{"value":{"entity-type":"item","numeric-id":944386,"id":"Q944386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$45C8501F-769F-4AAE-AE7C-85DA24CF58FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a2b2a8cf71a298beb3d5742fd0312db85012cf7","datavalue":{"value":{"entity-type":"item","numeric-id":579249,"id":"Q579249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$F604D96E-A9FE-45C5-9613-3E4E22B1EE15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c4fdc336b43063ea23854b1e9b2526543940aaa","datavalue":{"value":{"entity-type":"item","numeric-id":1044837,"id":"Q1044837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$D0BAD88A-F053-49FB-8FE8-B141C3B3CD15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7f579a1eff41f70abaa2adf98b1939988ff8b1a","datavalue":{"value":{"entity-type":"item","numeric-id":877259,"id":"Q877259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q276260$012A3CAD-A1A2-4737-A25E-3B61A2A47C8D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"252135ab2b407cc76a05b80c88eee9d7ebec28d8","datavalue":{"value":"10.1016/J.IC.2015.12.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q276260$5CCAEF86-4B32-4669-B00B-45C055117970","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e48a9df9d2466da0aef5a4c89861b5fcb730922e","datavalue":{"value":"The present paper further explores the connection between linear logic proofs (proof-nets) and the multiset based relational model of linear logic [\\textit{J.-Y. Girard}, Theor. Comput. Sci. 50, 1--102 (1987; Zbl 0625.03037); the first author et al., Theor. Comput. Sci. 412, No. 20, 1884--1902 (2011; Zbl 1222.03070)].NEWLINENEWLINEThe authors prove that it is possible to determine if the net obtained by cutting two cut-free nets is strongly normalizable, from the relational interpretations of the two cut-free nets. Moreover, being the former net strongly normalizable it is possible to determine the maximum length (i.e.\\ the number of cut reduction steps) of its reduction sequences, once more by only referring to the interpretations of the two cut-free nets in the relational model.NEWLINENEWLINESimilar questions apropos \\textit{weakly} normalization and the number of cut reduction steps leading to the normal form were answered in [the first author et al., loc. cit.]. The strongly normalization variant, not surprisingly, raises new challenges addressed in the present paper.NEWLINENEWLINEAs a consequence of the authors' semantic approach an alternative proof of strong normalization for Multiplicative Exponential Linear Logic (MELL) is presented. This alternative proof does not rely on confluence. In [``Linear logic and strong normalization'', in: 24th international conference on rewriting techniques and applications (RTA 2013), Eindhoven, The Netherlands, June 24--26, 2013. Wadern: Schloss Dagstuhl -- Leibniz Zentrum f\u00fcr Informatik. 39--54 (2013; \\url{doi:10.4230/LIPIcs.RTA.2013.39})], \\textit{B. Accattoli} also gave a proof of strong normalization for MELL which does not use any form of confluence. The novelty of the present proof is that it keeps the structure `weak normalization + conservation theorem', being the conservation theorem an immediate consequence of the semantic approach not relying on the confluence result.","type":"string"},"datatype":"string"},"type":"statement","id":"Q276260$9A5857FD-3298-4F93-AA33-9046B2052F35","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cf72fe02636f2b7949c7e24d01fc14cb8801819","datavalue":{"value":{"entity-type":"item","numeric-id":2958373,"id":"Q2958373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a75d41521b61d3d6e86e9dbd171b7059c000fb8","datavalue":{"value":{"amount":"+0.8846363425254822","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q276260$2A28AAC2-4A7D-48EC-AB89-4880886C1945","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1748af548a2db5d7d245a0ebb4650561cd1670ee","datavalue":{"value":{"entity-type":"item","numeric-id":4896506,"id":"Q4896506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"67a139222a8e358ee53c224910ef7e40405c42e5","datavalue":{"value":{"amount":"+0.8260290622711182","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q276260$0716FCF0-3810-43C0-BCC3-C1E8B90D9372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d030e8f341bf6c6bcffbd0907116afda04d6ce59","datavalue":{"value":{"entity-type":"item","numeric-id":534698,"id":"Q534698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cede760fdb90f2511c88bb42e31e541f0e6649a2","datavalue":{"value":{"amount":"+0.8232265710830688","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q276260$F9500263-F3B3-4BB5-B337-99CA40470A97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edf288d97bcbfd54f497c29d54c5db6fc93f37b3","datavalue":{"value":{"entity-type":"item","numeric-id":1044837,"id":"Q1044837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d736be1e267da1d0d563c322c0ec1abd200f01b","datavalue":{"value":{"amount":"+0.8087833523750305","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q276260$4C281061-EC1F-4ACE-B4E8-6F9F4D1FCDF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b6a301eeb40edd651b2d7cfecbbd2064712be98c","datavalue":{"value":{"entity-type":"item","numeric-id":5360213,"id":"Q5360213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d94aa700bfede4d8bad4cb6e3eb6ac38ec2e6cf","datavalue":{"value":{"amount":"+0.804565966129303","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q276260$035AB13E-A405-4E69-8FE6-A3275CF7D6E2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A semantic account of strong normalization in linear logic","badges":[]}}}}}