{"entities":{"Q1183598":{"pageid":1194347,"ns":120,"title":"Item:Q1183598","lastrevid":70205031,"modified":"2026-04-13T13:09:13Z","type":"item","id":"Q1183598","labels":{"en":{"language":"en","value":"Cut elimination and automatic proof procedures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 33414"}},"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":"Q1183598$B3EE2ACF-46D8-47BB-B245-8FEA3E19C991","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"85fe8946059639ca504839cff89ea14a123525c9","datavalue":{"value":{"text":"Cut elimination and automatic proof procedures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1183598$45770D46-3470-4738-837A-A41441DC9DC1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ca050b9380374aa53a636a184099b974ab03b584","datavalue":{"value":"0745.68098","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1183598$964CAB75-EA51-4A95-A0FF-BB37DB0F16D6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6e35baf944cbb7ce4bfffbb6f9bd6d0a83c65d26","datavalue":{"value":"10.1016/0304-3975(91)90086-H","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1183598$D644E347-3D8A-4E81-9F5F-BF69D8E6B7FF","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":"Q1183598$87686CDD-8261-43D3-9457-5E4F0728673C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"120787504bea9565def539fb4bfb19084956028b","datavalue":{"value":{"time":"+1992-06-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1183598$26ABD6CF-7F98-49A8-92AD-C97FC917EE54","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4930fdd0ce7e1f2e10d29a4f5cb1d98e404b2fcc","datavalue":{"value":"We first present a modified version of the cut elimination theorem and use an example to show that the upper bound (which is a function of the length of a proof and the complexity of the cut formulas in the proof) of the length of the cut-free proof given by the modified cut elimination theorem matches the length of the cut-free proof of the example. We also discuss the resolution method and some of its refinements with respect to the possibility of using cut. For each refinement, we give an upper bound (for the shortest cut-free proof) as a function of the length of the refutation. On the other hand, we give examples which show that the upper bounds are minimal. Finally, we discuss why the usual proof methods are cut-free.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1183598$6269F639-78D5-49ED-8498-202849E9B8B0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1183598$285D8BEE-9197-442F-BAD1-564FB080ADF0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78e6898b29a94106553ed11d419a28cfc491d9ba","datavalue":{"value":"33414","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1183598$D87A9FCE-AE29-4BB0-A320-A0D69E3B25A5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1183598$56EC1F9C-1620-43C2-9FF0-4914AB5EB357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"817f91d754a6618dd027e0d851a1fc8b7cbc7134","datavalue":{"value":"upper bound","type":"string"},"datatype":"string"},"type":"statement","id":"Q1183598$45311C43-5DDC-4B82-90FF-28E882D4F7B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1183598$DD3825A9-178D-4356-96F7-8A154FD02293","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"700a7ab3c2173bf5b546ffeb63a43807e035e8a6","datavalue":{"value":{"entity-type":"item","numeric-id":250171,"id":"Q250171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1183598$1A5E2C45-D5D3-4BFA-A131-47E016886796","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":"Q1183598$746BB5AE-7F58-4555-85A9-C7ADD4E697E7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae9d7e1a4422596c433e632b2dcd8392efe3ea66","datavalue":{"value":{"entity-type":"item","numeric-id":3667967,"id":"Q3667967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1183598$5A7F1BC0-5E5E-4B7F-8E08-26EF329E824D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cd44858abd76ba6a4654ef8a7945fafeb171c3b","datavalue":{"value":{"entity-type":"item","numeric-id":1057847,"id":"Q1057847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1183598$2A4A29B9-EF13-434B-8741-075A5DD43675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af9616b003d703f9d09294a2db2e4505eb229f58","datavalue":{"value":{"entity-type":"item","numeric-id":5310891,"id":"Q5310891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1183598$CC6756B5-CD28-4C54-8D52-F3F80DEE002C","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"b7c2ed7ceec8074de5e98d334baa84c604a07a54","datavalue":{"value":"Q127720171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1183598$95072190-2A14-4D58-B209-F79A89A9F690","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cfe35f01597c59a79d7085293ee38ec71a3c4d2","datavalue":{"value":{"entity-type":"item","numeric-id":5927981,"id":"Q5927981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"394e569aac5720dac146e9d0664ecbb7cbd7e3d9","datavalue":{"value":{"amount":"+0.8321300745010376","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":"Q1183598$1C9F3BF2-D44B-4E84-8F08-433A116129EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"191079e0016b981d445c12a9dd2d2b3251823037","datavalue":{"value":{"entity-type":"item","numeric-id":3816070,"id":"Q3816070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"394e569aac5720dac146e9d0664ecbb7cbd7e3d9","datavalue":{"value":{"amount":"+0.8321300745010376","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":"Q1183598$8B5C6648-2E84-4F5E-A7E4-5EB647F0511F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fe186cac75804def3c2fa703a831734e4da013d","datavalue":{"value":{"entity-type":"item","numeric-id":5361251,"id":"Q5361251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"264efddb3a46bc2ac5d4ccc6a4e75737c114b87f","datavalue":{"value":{"amount":"+0.821221113204956","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":"Q1183598$92A9EC7D-F611-4462-972C-5A04A142BDBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"abede1ff1a0be2900336d947290c1b6d50095efc","datavalue":{"value":{"entity-type":"item","numeric-id":2457341,"id":"Q2457341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd4819900d5004dbb10d9ce9024b7bafb99f1de9","datavalue":{"value":{"amount":"+0.8132901191711426","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":"Q1183598$B0AC10B6-514C-402C-B6DB-54070EC3BFC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3987f987c61a53d441911f6d6995e2961a38dc4a","datavalue":{"value":{"entity-type":"item","numeric-id":2253866,"id":"Q2253866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f43661e8b0bcd6b75d7708e36cbb4140f802f748","datavalue":{"value":{"amount":"+0.8104682564735413","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":"Q1183598$A6D91473-7B3B-4D22-8E0F-13C2D14E9CAE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut elimination and automatic proof procedures","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cut_elimination_and_automatic_proof_procedures"}}}}}