{"entities":{"Q1603701":{"pageid":1614441,"ns":120,"title":"Item:Q1603701","lastrevid":47944921,"modified":"2026-01-03T03:50:25Z","type":"item","id":"Q1603701","labels":{"en":{"language":"en","value":"A uniform semantic proof for cut-elimination and completeness of various first and higher order logics."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1767903"}},"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":"Q1603701$C427CBB7-87D7-47A1-AAA6-19C455078D8D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"409ba33d5caa386be9c50596ba5c641731589a3a","datavalue":{"value":{"text":"A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1603701$8ED57BE5-623E-4D2C-B2FB-B85C041EFC82","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e6754ff8a3ab5f2a558a58faf9d81de7b716f21f","datavalue":{"value":"1048.03042","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1603701$E3B31713-B184-4522-B377-B156AE3EE1B3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f9722631ee22f7decd553d47d860ed15b59d7d93","datavalue":{"value":"10.1016/S0304-3975(02)00024-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1603701$8712A9DB-9C1B-4EAA-9962-15D2E9412889","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b26cd3ce2ca6a508af647c0b8ee8a10745379af0","datavalue":{"value":{"entity-type":"item","numeric-id":235600,"id":"Q235600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$FDB829A4-261F-47DC-8792-4E4DE9619F24","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$B35BAE55-B932-4731-B1C7-39742CA37CE8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eb77668c0bac74ac5ea553fa2146ed5e736444f1","datavalue":{"value":{"time":"+2002-07-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1603701$24D5D53C-33D5-4CBA-8593-9A9BC70C7847","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1a5799e475de61dbe246f23d10c90153b99e125e","datavalue":{"value":"We present a natural generalization of Girard's (first-order) phase semantics of linear logic [\\textit{J.-Y. Girard}, Theor. Comput. Sci. 50, 1--102 (1987; Zbl 0625.03037)] to intuitionistic and higher-order phase semantics. Then we show that this semantic framework allows us to derive a uniform semantic proof of the (first-order and) higher-order cut-elimination theorem (as well as a (first-order and) higher-order phase-semantic completeness theorem) for various different logical systems at the same time. Our semantic proof works for various different logical systems uniformly in a strong sense (without any change of the argument of proof): it works for both first-order and higher-order versions and for linear, substructural, and standard logics uniformly, and for both their intuitionistic and classical versions uniformly.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$EFBE8EC5-D55A-42C2-8ECB-AF1DEE705FDB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1603701$87EB1F8F-9DC9-43A8-B292-6919E06C2452","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1603701$B28A4111-81B0-4D82-AFBB-9FD1C688D6D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1603701$92245A6B-8091-4702-B084-8E5A14B67969","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"64f850875b15f5fceb79ead7c5e5316cbbbd8cf5","datavalue":{"value":"1767903","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1603701$C214307E-91E7-4097-9A62-3BD2B4FB6429","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6296b59146c0756f86a4521eecba6a21b3c72498","datavalue":{"value":"generalization of phase semantics of linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$CEF382FA-0A16-41CB-804B-46841978A9CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"abf8c0eacd4cc8fa0141e08e7b78bb3130515692","datavalue":{"value":"higher-order phase semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$A3DAE8AF-227B-417D-8487-2F673D68C8E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$7D806423-1A70-4052-B767-FB6193DC2EF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$0A55898F-207A-44F0-A35E-A4A92DC72C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e19a56a35da34eb08b4ac43272212a5013c8d21","datavalue":{"value":"substructural logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$B46B1C74-5BBB-4915-ABA8-8ABD2BA1E711","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1603701$BD5E2D1C-A41B-4948-AEEF-AA1458F9CD69","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":"Q1603701$02B030DC-4A08-4244-A8BC-A079B94CCD19","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"babc13e0719d02ac80e7d11ecc8370e0ef2774b2","datavalue":{"value":{"entity-type":"item","numeric-id":4694232,"id":"Q4694232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$67C17868-718A-4AE4-93E4-E3E5EA7FE2FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da6f93665c2e557c57ca467a92e979922ef9ed2b","datavalue":{"value":{"entity-type":"item","numeric-id":3971583,"id":"Q3971583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$86E5BFC2-B534-4296-902F-A7BF60A1E24C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aaa1e1e1a7f2285ef58a648d10db096ce5882504","datavalue":{"value":{"entity-type":"item","numeric-id":5057474,"id":"Q5057474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$C2910E7B-1101-4BC7-B4F0-DA7C07E02485","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5345f6943b27d982604103a8a31c0b3f8701a43b","datavalue":{"value":{"entity-type":"item","numeric-id":4077989,"id":"Q4077989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$3154FBA5-13E3-4E75-A5BE-C4886C41794F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea08311e5cede8e103fdccb0049502f7fb72a285","datavalue":{"value":{"entity-type":"item","numeric-id":1264140,"id":"Q1264140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$9EC2CA95-DE36-4D7E-AAFA-21AEBB92B9A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7efca8e4596d9afd2a5ad9c3a14e955093b5ab3","datavalue":{"value":{"entity-type":"item","numeric-id":4039813,"id":"Q4039813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$9F767872-B0F8-497A-AA28-1E81D394FC63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e8b681055e76d6a26f65d45cdc8c5755ebf47fc","datavalue":{"value":{"entity-type":"item","numeric-id":3481700,"id":"Q3481700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$C82A20B0-3196-4422-A0EB-73B61163D4EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e1600269660202da6f1411b0b357c46eeb2d096","datavalue":{"value":{"entity-type":"item","numeric-id":3475264,"id":"Q3475264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$CEC86FEA-50FA-44B4-9C3D-9969281823B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54351e142ba78301c80d7c3516f9734aa8ddee58","datavalue":{"value":{"entity-type":"item","numeric-id":3791120,"id":"Q3791120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$12D0C455-6296-4F8F-A105-6C2BA3C1DB6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c981e1f87c605bc2771b1a302028511e8fc3dd72","datavalue":{"value":{"entity-type":"item","numeric-id":4842966,"id":"Q4842966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$70A1971F-BC11-4C93-8945-E30389ECD7A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a48c61c6138784426830f34f60c6e6c51b112861","datavalue":{"value":{"entity-type":"item","numeric-id":4842976,"id":"Q4842976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$B2F6FE5A-E54B-4261-8A25-044EA91002F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5de5a92891dc05a0b1130c4f428cc2540c07d8c7","datavalue":{"value":{"entity-type":"item","numeric-id":4382470,"id":"Q4382470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$65BB4664-22C3-4577-B588-730DECB352E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb84102d559fd7a0d70d66cd908e0bdc3f41ec08","datavalue":{"value":{"entity-type":"item","numeric-id":1917079,"id":"Q1917079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$3C86010C-393F-49E9-9EB7-532B9C55F331","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2eebdcb126c2a053de33545bd3e4688ccc3b0d15","datavalue":{"value":{"entity-type":"item","numeric-id":4222841,"id":"Q4222841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$E5518531-7314-4ACE-8AC1-9A4E0272F7AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeade2cfdcfcd253e188a74e9e8eaa51de1f1876","datavalue":{"value":{"entity-type":"item","numeric-id":1575865,"id":"Q1575865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$B25C3288-7B44-4E70-AA5F-5A02E33CCCCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb284231feaca1ff69e1057ce8b481c1f7a89810","datavalue":{"value":{"entity-type":"item","numeric-id":4703047,"id":"Q4703047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$FDB2EC7F-E8A8-4CB6-86ED-37A9B68856E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76e93ef4dc600baabf1caa2d6a4d97f42bc019d1","datavalue":{"value":{"entity-type":"item","numeric-id":4262585,"id":"Q4262585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$DE1819A7-2D88-49B4-A533-6A95FCD1F218","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c444c6ec3cb9757a686662251d3648e5a1703ba","datavalue":{"value":{"entity-type":"item","numeric-id":4940727,"id":"Q4940727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$24DB7B24-6239-45ED-AEBC-318D39FE63B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc09538a5c77707bd740c1af4339f9cfde82b8b","datavalue":{"value":{"entity-type":"item","numeric-id":3707997,"id":"Q3707997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$6B9FAFF4-EA71-4814-AD13-8D12B72C44C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"341cf25e1331e9c3d9b625066b41f81f88fc1449","datavalue":{"value":{"entity-type":"item","numeric-id":5549033,"id":"Q5549033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$0682498A-6834-48EE-8040-FD635B7A66CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcd018ec321bcf4f814daa12e1f34e1a42f18475","datavalue":{"value":{"entity-type":"item","numeric-id":3832536,"id":"Q3832536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$F8615E44-BB1C-48A9-9757-AA7601D102D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a6b93763c3bee209b670cc606716e146a89ae81","datavalue":{"value":{"entity-type":"item","numeric-id":4858821,"id":"Q4858821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$0DD091CA-78CF-45AF-880B-D668391524AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e21aa2c8417444bb3098b83ec743e607734c3bfb","datavalue":{"value":{"entity-type":"item","numeric-id":3285631,"id":"Q3285631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$B2AF0FF9-6500-4FAE-961F-E7FB9D64D07E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6424e891ec3320cd9100f08f39833a24c09ba9b7","datavalue":{"value":{"entity-type":"item","numeric-id":5596744,"id":"Q5596744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$BF710DE0-4BA0-4173-9ADD-BE78A7605DF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c7130b8e8ad403bac4e3a609004e5598d1175d3","datavalue":{"value":{"entity-type":"item","numeric-id":5561939,"id":"Q5561939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1603701$A09B0BFB-FA30-49E7-A6F3-57D1E44312AF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8235d23e6d6d2cf5ce97f5110424a8673a3b15b9","datavalue":{"value":{"entity-type":"item","numeric-id":4222841,"id":"Q4222841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab45e9f7077a64882c441d1a622c6dc492d1966e","datavalue":{"value":{"amount":"+0.9159523844718932","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":"Q1603701$227F9C4A-3716-471D-8C47-EF6F796D7533","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"418f04edcf11ec662a481924a0aaf5060c05f5fa","datavalue":{"value":{"entity-type":"item","numeric-id":1575865,"id":"Q1575865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4b9259a0ecb1618f46c58ee7206faaee176fd74","datavalue":{"value":{"amount":"+0.8870162963867188","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":"Q1603701$FF213760-892A-4FCC-9221-908DEB77CEAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47adc29f5016c79fa420997aa20f4e099a89c304","datavalue":{"value":{"entity-type":"item","numeric-id":1901891,"id":"Q1901891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f004c94dffb1f21dc303491f76e43d458995535","datavalue":{"value":{"amount":"+0.8870158791542053","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":"Q1603701$F5CEAB31-07EB-4E8E-95AD-3EC12AC67E76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62ae42a808b37199a642114f619618f8a831d761","datavalue":{"value":{"entity-type":"item","numeric-id":2640596,"id":"Q2640596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3dd6c21906ec17c81bc14f47491ab63c40fa2244","datavalue":{"value":{"amount":"+0.779122531414032","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":"Q1603701$A8428138-96ED-4444-A94D-C38BFF79A6F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa561b8b5342ab318639cadc68c91a52aafd256f","datavalue":{"value":{"entity-type":"item","numeric-id":3475264,"id":"Q3475264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd1a7b1fd50fb64b79a2bf4c62af4db585009810","datavalue":{"value":{"amount":"+0.7748823761940002","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":"Q1603701$2619976F-A5EA-4495-ABD2-81B609C0069E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1603701","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1603701"}}}}}