{"entities":{"Q2708321":{"pageid":2719060,"ns":120,"title":"Item:Q2708321","lastrevid":47599774,"modified":"2026-01-02T04:40:43Z","type":"item","id":"Q2708321","labels":{"en":{"language":"en","value":"Strong normalisation of cut-elimination in classical logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1588179"}},"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":"Q2708321$575F1147-324A-4925-8BFA-BE75F4C1D4AC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b32d1b8cca285124b50e5c5d62718a3dea5a2683","datavalue":{"value":"0982.03032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$AEBA3F7A-3410-41DB-A1D5-CBF3E9E4C0DA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c142bfdb3ba24d15560e9f10bd1352974c97a2c9","datavalue":{"value":{"time":"+2002-03-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2708321$EB094E7A-8B09-44EF-95CA-96560B7BA864","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$9EBD27A5-0C86-470C-A5D2-4B71B27127E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$904AA047-2ADE-4AFE-BF72-DAF03D885DC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$1921FEA2-3DF5-49B2-8979-59A76A9F1F29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$1AD682A9-8632-4991-9EA5-99B1331433BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$5998FC06-8C40-4094-929F-A36B29CED704","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"12580c63f2151526c8a587c89fbb12a7e31dc936","datavalue":{"value":"1588179","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2708321$202D528B-10CA-414D-A123-417884755ECC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00134f94fae617052450fe78ce4e8e7c792fddd5","datavalue":{"value":"normalisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$906F143C-B58C-4280-B4FB-C5EDA6297343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$D0E84B08-E5AB-48B1-A887-D787A4D5306F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dbadd689afdff7de47d6fc9658b887b8542f7df4","datavalue":{"value":"contraction rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$79953A1E-3111-4537-91DE-0C7ABDBF3DA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$E4B879A2-E83C-4A22-B829-3E9F3E3DBC31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"90f741c3fde794dd728426723cc0fffb883a118d","datavalue":{"value":"notation systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$ECBD8FFC-382E-4DD6-9E51-E5331EB6A572","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$DBA08421-564F-4941-AB39-7E8EA2FF70C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"41e62a60518465f7bb44a163681aecd44c7753e6","datavalue":{"value":"term-rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$EAF72B79-C052-425F-B5CB-6DC27D81381E","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":"Q2708321$5E73300C-A466-4D0C-8900-F3354E332866","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"342bc527848ca7a42df8ff6d1a755158d361e74c","datavalue":{"value":{"entity-type":"item","numeric-id":681347,"id":"Q681347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708321$4529A734-ED8C-4830-AF37-5E2D71887DEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"38c1f622ca5a8e1981406df5479b2fddfe8cfc72","datavalue":{"value":{"entity-type":"item","numeric-id":1575876,"id":"Q1575876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708321$5A29A771-A4DD-4389-89C5-76E781BA755A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6074c0bbcd04e14480b07b3d4771f52056452529","datavalue":{"value":{"text":"Strong normalisation of cut-elimination in classical logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2708321$EF51FE6E-AF4A-4451-8193-F6868C90A1CB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1529db038bde6a8aed76ac5e8432917aee1a9200","datavalue":{"value":{"entity-type":"item","numeric-id":2803574,"id":"Q2803574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708321$5CE83C68-CE80-49F6-ACFE-5F240A50FDAC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0ebe33c5c52a110efabf716945a25e8be666df18","datavalue":{"value":"In this article first the fact that cut-elimination for classical propositional sequent calculus is, in the presence of explicit contraction rules, not strongly normalising, is revisited. The authors look at various attempts in the literature to remedy this by adding suitable restrictions to the cut-elimination procedure, and criticize them as being too restrictive. Then an interesting notation system for denoting sequent calculus proofs is introduced. This system is some kind of lambda calculus, with the possibility to abstract both on the left and the right side of a sequent. Reductions are introduced, which correspond to cut-elimination steps and are similar to \\(\\beta\\)-reductions in the lambda calculus. It is then shown that the resulting term-rewriting system is strongly normalising. Finally the notation system is extended to the classical first-order sequent calculus, but the proof of strong normalisation is only sketched for that system.NEWLINENEWLINENEWLINEReferences: \\textit{J. Gallier}, ``Constructive logics. I: A tutorial on proof systems and typed \\(\\lambda\\)-calculi'', Theor. Comput. Sci. 110, No. 2, 249-339 (1993; Zbl 0772.03026); \\textit{V. Danos}, \\textit{J.-B. Joinet}, and \\textit{H. Schellinx}, ``A new deconstructive logic: Linear logic'', J. Symb. Log. 62, No. 3, 755-807 (1997; Zbl 0895.03023).","type":"string"},"datatype":"string"},"type":"statement","id":"Q2708321$92D827BC-DA56-45AB-86CF-B46F8F16EEA7","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"df6d145faee35a3a1d4d9e701f68880611a87159","datavalue":{"value":{"entity-type":"item","numeric-id":587965,"id":"Q587965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2708321$341C0F68-39A1-4D29-B743-03A6C6C863E8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cc53e3d08fd24c4593c7add0ca77cced95343d2","datavalue":{"value":{"entity-type":"item","numeric-id":4263882,"id":"Q4263882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cfa81128455ca56f380805ff05ef1c5fa3807fdf","datavalue":{"value":{"amount":"+0.8860669732093811","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":"Q2708321$083ACFDB-8BE2-4DCA-9A01-1041F1E8A10B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a379be0807c0684d3c8b85e371369487a0e89e65","datavalue":{"value":{"entity-type":"item","numeric-id":2778837,"id":"Q2778837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b998821404f4ea2377853f770251e902e4f9a38","datavalue":{"value":{"amount":"+0.8641815781593323","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":"Q2708321$8712081B-BA9A-4CF9-A365-7D7F15F30A18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"34ecf3b9dfd6a0e5496fe9d491fee29829fdc2de","datavalue":{"value":{"entity-type":"item","numeric-id":4650284,"id":"Q4650284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2935d7506f5bceb4d14f084da3a713976fed2077","datavalue":{"value":{"amount":"+0.8378865122795105","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":"Q2708321$BCAC4635-74C1-47A4-8614-8C6CB247CF3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d45c7dff42ba9946e9a8acd3e138332c15ef18e2","datavalue":{"value":{"entity-type":"item","numeric-id":1902976,"id":"Q1902976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8f6ac985237c70d3d162c0f5336dedf60d1dc15","datavalue":{"value":{"amount":"+0.8252987861633301","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":"Q2708321$0B56B564-B207-4015-872A-B7B763B8EB27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a05d1e4cf7be38fc77d12fa1ba22b8449464125","datavalue":{"value":{"entity-type":"item","numeric-id":5458374,"id":"Q5458374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44df6a820f356a21e4572c233649156048826742","datavalue":{"value":{"amount":"+0.824216365814209","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":"Q2708321$08F5061A-42FF-4F92-889F-38602C16A086","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2708321","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2708321"}}}}}