{"entities":{"Q1345901":{"pageid":1356640,"ns":120,"title":"Item:Q1345901","lastrevid":68520039,"modified":"2026-04-13T00:15:26Z","type":"item","id":"Q1345901","labels":{"en":{"language":"en","value":"On the linear decoration of intuitionistic derivations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 734552"}},"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":"Q1345901$A6EBB193-E740-41D3-8160-0562DEF766CE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2c086fd8b8cfdfc1bf3928cba5ace5560dbac6d0","datavalue":{"value":{"text":"On the linear decoration of intuitionistic derivations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1345901$44EF3C41-34FA-449A-A61E-767747A5F66B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"24b2a8328f6e580f7876282722102ae1268828d7","datavalue":{"value":"0820.03036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1345901$BBDC699D-AC97-4CAF-88A2-572A407A412D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"58bc68810e06b3f31b043e66df90c0ec51d9dd9a","datavalue":{"value":"10.1007/BF02390456","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1345901$8219568A-F0FC-4916-9186-EFD759E010D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"93999ca0789e250fb0db50708f38a31742036836","datavalue":{"value":{"entity-type":"item","numeric-id":550252,"id":"Q550252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$168809D3-DBF1-4824-90E5-0518731A9CD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4525c955b47badf335bb39d178a4075baf3a0250","datavalue":{"value":{"entity-type":"item","numeric-id":1345899,"id":"Q1345899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$FB09F5BA-4FCE-4474-AF52-0966AB9199FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"991173f2ea22332135ad6abd3f0c984815ecedd3","datavalue":{"value":{"entity-type":"item","numeric-id":1345900,"id":"Q1345900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$6A1BC77F-A812-4A3B-8D80-8CEB50D5B4F2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$EB3877D8-C335-40F8-8E00-9F95BBE2A903","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5a1529ffb26db2b22f3624b5eae79e54a7bbf813","datavalue":{"value":{"time":"+1995-09-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1345901$15444361-3026-4CB8-9EBD-0829147352E1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"6d483c4784a0f6bceb676432209421606dc83639","datavalue":{"value":"Uniform translations of intuitionistic into linear logic, with their plethoric use of exponentials, are bound to give only `universal linearity information' about proofs. This paper aims at displaying the structure of `specific linearity information' hidden in a given derivation by constructing a proof-by-proof embedding of intuitionistic sequent calculus into linear logic such that:   (1) the skeleton of the original proof is preserved (the linear proof is a `decoration' of the intuitionistic one),   (2) each exponential in the image is necessary, as it is required by some instance of a contraction or weakening rule somewhere in the proof.   A notion of `lower decoration strategy' is defined, which for the neutral intuitionistic fragment of Girard's `Unified Logic' (LU) results in a subdecoration of the uniform decoration obtained using the well-known translation of intuitionistic into linear logic. In fact, the linear proof obtained is an optimal linear version of the original LU- derivation, with essentially the same set of reductions.   This is the first in a series of papers, all of which make use of linear logic as a proof-theoretical tool. An in-depth analysis of the normalization of classical sequent calculus is given in the sequel ``A new deconstructive logic: linear logic'' (to appear in J. Symb. Logic, and available via anonymous ftp or at http://boole.logique.jussieu.fr/www.hars/djs.html).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$775DBA64-9E53-4CA2-94AE-CBAF5AFCABA2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1345901$CB48EDBB-509B-4CA9-BC3D-A6ABAE6EE505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1345901$39FBA717-0CE6-4069-A26F-2F9E008A7634","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"46e4bc271b417629cbb99f82f92ee96011f49f70","datavalue":{"value":"734552","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1345901$660BAFC9-EC4B-427C-9E53-301363188F97","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$8C4F84AA-1F18-4D45-8BAD-717F370EE2B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$7B6A0F3A-15DE-4F7A-A2E4-E47425597A82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"91a6cd16682fdee3705d64b127e7d12cf26a3690","datavalue":{"value":"unified logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$93B7C1C4-5DAA-44EA-9529-33B85660506F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$F6F1D030-2D94-42F0-9C9C-51CFAE5E677A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"37cb51e682c5d324999ff82c0034fb71030cd231","datavalue":{"value":"proof- by-proof embedding","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$B5A869C3-DDB0-4BD9-B5F3-00969B16AB85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8cd5a0fc8524d164d5f2bf08c2ab6fbd4c6ec28e","datavalue":{"value":"intuitionistic sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$83DD01C1-9AC9-4A2C-9F6D-E2C255986552","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14a6728e50cbaca75cf287bc48ae14f636315ae3","datavalue":{"value":"translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1345901$9AA47D9E-0608-4392-9695-D37E1E7CA481","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":"Q1345901$E8AE6DD5-55F6-4127-99A9-D9A12254F23C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d0c3c520266c0eb0c8719af10bc93260259779f","datavalue":{"value":{"entity-type":"item","numeric-id":4842975,"id":"Q4842975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$884A2A1F-645B-4D92-A254-806D1E97A128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b118fc85ee391a10c7ec87ba8e392cc631a1eaa0","datavalue":{"value":{"entity-type":"item","numeric-id":4282602,"id":"Q4282602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$FCA2464F-5F1B-4572-A0D8-68E3056AC93D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e84ff42267477e949575e937efae295817dbcbf","datavalue":{"value":{"entity-type":"item","numeric-id":4372906,"id":"Q4372906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$F64EA9EF-3371-44A2-8037-2703703B7E2F","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":"Q1345901$D383D1CA-BEAB-4DA1-BEC5-9AD2F86C8AF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14fba5e8ace22a05b3ebef9aa0392420cd4ad549","datavalue":{"value":{"entity-type":"item","numeric-id":685059,"id":"Q685059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$43D1CD3F-6631-4D94-97CF-D555B3342363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"106507d2ad7198eda87b14657c5af01d30112965","datavalue":{"value":{"entity-type":"item","numeric-id":4474830,"id":"Q4474830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$A4AEBDD3-8777-465D-AD30-97E504EBDF20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c7312367626057a1ed18ce459375f7ee2aab280","datavalue":{"value":{"entity-type":"item","numeric-id":3986870,"id":"Q3986870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1345901$0A0E1EA9-F5B7-4D0D-8BDF-39739E42A9F9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"298f54efda5b32e5a22511da7f85bcfbab77615c","datavalue":{"value":{"entity-type":"item","numeric-id":2702566,"id":"Q2702566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75d989676605eaaa8af6f2802806f21dc727e94d","datavalue":{"value":{"amount":"+0.7870423793792725","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":"Q1345901$0C1F6E03-348C-4AA5-949F-1115267E0C54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"21ea86ffc61316ca43e87cd26e310126220d364d","datavalue":{"value":{"entity-type":"item","numeric-id":5688803,"id":"Q5688803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"988f79c941e7a48b5342f13b5aff343cf2b07ff7","datavalue":{"value":{"amount":"+0.7856484651565552","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":"Q1345901$0595DE94-85EE-4052-994A-4364E658659C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a1c1bb59fd9363bdacd386fc7141e51a81d0525","datavalue":{"value":{"entity-type":"item","numeric-id":1407574,"id":"Q1407574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e9790f4a7ff12bea2fb7fdbd21cbbb60439e731","datavalue":{"value":{"amount":"+0.780580997467041","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":"Q1345901$97C0E0C1-C069-4B4D-9E3F-6AB09FB30744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72f4eaeb4480d971e949b0a2fbd8d8001d316a66","datavalue":{"value":{"entity-type":"item","numeric-id":4882488,"id":"Q4882488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d21a88abc1e43b9df4346a8a365b002f3ebac0df","datavalue":{"value":{"amount":"+0.7705361247062683","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":"Q1345901$6C882414-B33B-4D0E-A784-D890D33CEF1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4c2f2f39a0c695dbffa7d725e1703c49ea94757","datavalue":{"value":{"entity-type":"item","numeric-id":1891252,"id":"Q1891252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76cc74b2e677efdd9b731811c7bcf38fa9dc926b","datavalue":{"value":{"amount":"+0.7696606516838074","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":"Q1345901$A2BEFB11-477E-46BE-B7B5-EA90D7D34FCF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the linear decoration of intuitionistic derivations","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_linear_decoration_of_intuitionistic_derivations"}}}}}