{"entities":{"Q817704":{"pageid":819552,"ns":120,"title":"Item:Q817704","lastrevid":49801495,"modified":"2026-01-10T20:59:21Z","type":"item","id":"Q817704","labels":{"en":{"language":"en","value":"Towards a semantic characterization of cut-elimination"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5013038"}},"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":"Q817704$67439783-0D09-4182-A3CA-8069C29F1697","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8043bc20ea3f1780c95061613af7b141c0d540da","datavalue":{"value":{"text":"Towards a semantic characterization of cut-elimination","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q817704$2D77493F-354C-46CF-A35B-41487DB16A0D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"20b35d2c234fa91b48bdb9001226da963d04a1e8","datavalue":{"value":"1105.03057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817704$4C2D8586-64B7-4977-B1AE-A05073660FB3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb4465c1e4c8de201e147387c933ac41a7d412d9","datavalue":{"value":{"entity-type":"item","numeric-id":385018,"id":"Q385018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$891FBD6E-3887-44F1-ADCC-3CC85A11930C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e02fd546ce8d461240920d62f3603cf121b4693c","datavalue":{"value":{"entity-type":"item","numeric-id":271691,"id":"Q271691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$1B4F632F-7622-4D86-9C46-5C3B48EE8F31","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$8DC32AE4-AE7C-4DD3-8B24-C0478DC58B25","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"46a32b96026a1aa43ce9bf7d3e87290deb94d5e1","datavalue":{"value":{"time":"+2006-03-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q817704$0E35A173-57DE-4F69-A6F6-9665C6747B64","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"70235f771ea1e5ba8a46f33cbead67158d978101","datavalue":{"value":"An occurrence of the cut rule in a derivation is called reductive if either (i) both cut formulas are the principal formulas of logical rules, or (ii) one of the two cut formulas is a context formula of a rule other than the cut, or (iii) one of the two premises is an identity axiom (of the form \\(X\\Rightarrow X\\)). Reductive cut-elimination for simple theories has been given a syntactic and a semantic characterization in the paper under review. A sequent calculus is called simple, if it is a single-conclusion calculus that contains some identity axioms (mentioned above), the cut rule, structural rules, and left and right logical rules for each logical connective. The syntactic characterization reads as: a simple theory admits reductive cut-elimination iff   (1) its logical rules are reductive, i.e., if \\(\\Theta\\Rightarrow A\\) is deducible from \\textbf{S}, and \\(\\Theta_1,A,\\Theta_2\\Rightarrow B\\) is deducible from \\({\\mathbf S}'\\), then \\(\\Theta_1,\\Theta,\\Theta_2\\Rightarrow B\\) is deducible from \\(\\{{\\mathbf S},{\\mathbf S}'\\}\\) using only the identity axioms, the cut rule, and the structural rules; and   (2) its structural rules are weakly substitutive, i.e., every instance of any of them is derivable within the calculus.  Also a semantic variant of the above characterization is presented (for reductive cut-elimination) in terms of pre-phase structures.","type":"string"},"datatype":"string"},"type":"statement","id":"Q817704$4F830357-9816-4510-BFB5-78C927E6EC23","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817704$CC53FC08-2D30-4169-BE7A-5C9602BD1DE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b363e494c684597e57f0cc15c7c0d8f9f3bcf9fc","datavalue":{"value":"03B47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817704$771C7DBF-FF5C-4A61-AF9F-441AA90422E4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d9abf90c364c379536e27fb7451e69e5635f1466","datavalue":{"value":"5013038","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817704$F5B55BEA-24DE-4EC2-99D4-DAF5EF93FDFA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q817704$0B368D4F-CD9E-4E93-A081-F3D1C9917F12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q817704$F7DAE677-464B-4494-B98D-97074F7DA5C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82f58749215346b108a3924805b4196cdbb9ed80","datavalue":{"value":"nonclassical logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q817704$36D4B513-E394-4DB0-AF65-675B69516A4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7261777472d4a441f436b868f2c61d8d67ac5d8f","datavalue":{"value":"substructural logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q817704$24216D04-2A9D-49E8-B27C-08C95409C9DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0330316506ca239cfff19d0e3df96793e84e6ecd","datavalue":{"value":"phase semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q817704$23D520CC-8AFF-4D97-899E-05BCCA5208DE","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"4bc285a01ee2fee3db93f6df1148b69669dc8b6e","datavalue":{"value":{"entity-type":"item","numeric-id":590045,"id":"Q590045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$994DAECA-1C70-484E-BBFF-1366B5E3F0FB","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":"Q817704$9B48102E-ADB9-4328-87B0-F222F178D5A1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fd9fbded5f57191c8cef56e0f11b3145025f7599","datavalue":{"value":"https://doi.org/10.1007/s11225-006-6607-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q817704$A9092E49-9D01-453F-8DCF-389EC7ED5BFC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"73161f487070ddcd28432c5e9b57c5f15a10b077","datavalue":{"value":"W2166144087","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817704$2A19D41F-5848-438E-82DC-29FAAC2C7151","rank":"normal"}],"P223":[{"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":"Q817704$C1102334-EEB4-4253-83C8-F1B142AE99E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38e1d811262dd8c2250bea4bc0f676125b4798fd","datavalue":{"value":{"entity-type":"item","numeric-id":4539639,"id":"Q4539639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$647FE81C-285E-4307-92CB-6FF4C8111A2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"607032864cb06dec4fa711d9a8c97f9a6304f17b","datavalue":{"value":{"entity-type":"item","numeric-id":1770974,"id":"Q1770974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$1A2042DC-5FA1-4DC3-8473-7B945C5FF57C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b70c7b3f003527069c2310fc828f8afaad5df5d6","datavalue":{"value":{"entity-type":"item","numeric-id":1838471,"id":"Q1838471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$30FF429F-CC56-4AEF-A6E8-AAEB0B8A4838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2ea905e0dd45e5f666435e07c5347d2d8ec010b","datavalue":{"value":{"entity-type":"item","numeric-id":4215630,"id":"Q4215630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$67706A04-B88A-4750-81CB-E51089D6336A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"749aa5c484d884771466997b802e7dc39af08a46","datavalue":{"value":{"entity-type":"item","numeric-id":5311280,"id":"Q5311280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$3DF23F14-3B48-4E3B-B970-84FE9B70AFD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$796E8A1E-11C6-4928-A68D-C36567D9E826","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"51cc071a63d7e2256ef91f1a5892cb76da195303","datavalue":{"value":{"entity-type":"item","numeric-id":4128539,"id":"Q4128539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$84F87D61-0F5B-4AA0-BD8C-1AD28E793987","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$6EFD5EF9-897F-4061-B17C-5A8A341F4A40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$8A4A161A-705D-44C0-ADB1-80044CF267A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c503eec55a1ac4f23ca138b62a55de1f3e0067f","datavalue":{"value":{"entity-type":"item","numeric-id":4263837,"id":"Q4263837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$DB9E29E6-C995-4DC6-A559-72FFC156704D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"613196c1ebb5efd26c81cbdcd44f5b10522db4db","datavalue":{"value":{"entity-type":"item","numeric-id":1344438,"id":"Q1344438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$90138CB9-8B05-41D2-A700-41172919CA0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"018b2c7d86bd03f8412e1acf9a71f1d8637d2a96","datavalue":{"value":{"entity-type":"item","numeric-id":4412848,"id":"Q4412848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$2110CB9C-BCE5-417A-819D-92F9F8A71744","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":"Q817704$283B6F6D-FF4A-43BB-A046-DE97926FDC16","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":"Q817704$88283A01-F049-457C-AE98-C64D3CCC1925","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76c47ac64788248a40d8543304d3dd3bc25cb13b","datavalue":{"value":{"entity-type":"item","numeric-id":1603701,"id":"Q1603701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$3081688C-9116-473E-8338-A0B54628AD51","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":"Q817704$DEB208E7-2194-406B-AF5E-BB576BC79DCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1785c5247614edefd452dd242bbf025baf6dd7dd","datavalue":{"value":{"entity-type":"item","numeric-id":2563461,"id":"Q2563461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$8E27EFB2-C5AE-4A7B-9716-C639715308FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"566b0c163a36b7b7dabcdd14884ed1324b40841d","datavalue":{"value":{"entity-type":"item","numeric-id":4805593,"id":"Q4805593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$1A968C98-409F-4C4B-B9F4-49B95A75E270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$72A950C6-E21C-474D-BDB9-FFA236CC80A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"556023de527f0a47926ace58f6081826c5c14adb","datavalue":{"value":{"entity-type":"item","numeric-id":5422301,"id":"Q5422301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817704$A8DC5F6E-6403-4F96-A8C3-0A0E96C02618","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"16de03b18a45df3e36554bb8d50e557935f2bb20","datavalue":{"value":"10.1007/S11225-006-6607-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817704$DAC390A3-F9EE-4F46-92AE-0FF6C584C025","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7910f50ae5a96092eb3bdfb8702ba88ad922a5f","datavalue":{"value":{"entity-type":"item","numeric-id":2259012,"id":"Q2259012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"540002b95f16f279ac88493f2561f6063f421b34","datavalue":{"value":{"amount":"+0.7658481597900391","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":"Q817704$2CA8730F-9815-4709-96C0-D949BEB89AB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ffab1ec510f63ff1e2a9542c3c3be4322ba4905","datavalue":{"value":{"entity-type":"item","numeric-id":5704011,"id":"Q5704011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87d4fc8113fdbc0ab9fb548b8133240235fee8c2","datavalue":{"value":{"amount":"+0.7585872411727905","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":"Q817704$8D1C741F-8E2C-4556-8440-9CA97B4B75AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bea16cd865d4882ee157d0dce3c18d98abc3ab7","datavalue":{"value":{"entity-type":"item","numeric-id":5458060,"id":"Q5458060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9836ff61f9692970e1d9819409cdeaa91dec262","datavalue":{"value":{"amount":"+0.7565290927886963","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":"Q817704$B1592FC1-B2F7-49E9-A932-F4CA66111967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf860819a7d9e00e8ecfc66b9e54f67135b51fe0","datavalue":{"value":{"entity-type":"item","numeric-id":5111901,"id":"Q5111901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"194837be703ecfddc04e72ee24e32123d3fb144f","datavalue":{"value":{"amount":"+0.7437931895256042","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":"Q817704$31CFC25D-92E4-4CEC-918D-84DDF4A1B071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51656c76c992c1a0edd06e476466ecbe6b5ae5a4","datavalue":{"value":{"entity-type":"item","numeric-id":4254567,"id":"Q4254567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ead7d9bbf155b45ead17f760dd64a2a0ce4f5b80","datavalue":{"value":{"amount":"+0.7421131730079651","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":"Q817704$0F21A1BB-C0A5-4412-9375-0AE15ED508A9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:817704","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:817704"}}}}}