{"entities":{"Q1302302":{"pageid":1313052,"ns":120,"title":"Item:Q1302302","lastrevid":67324887,"modified":"2026-04-12T16:52:02Z","type":"item","id":"Q1302302","labels":{"en":{"language":"en","value":"Cut normal forms and proof complexity"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1340820"}},"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":"Q1302302$42A3D5D3-4044-4C1C-A0BB-4D60B3959CFA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a63ba8416eb41e7c813f2dee0b12e04bab405e36","datavalue":{"value":{"text":"Cut normal forms and proof complexity","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1302302$5C6D867E-853A-416F-B0D9-4049696B754C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"36361a25fa158ddf348b9fc03764d6d52233e6ea","datavalue":{"value":"0940.03062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1302302$1CCEAF11-74DD-4C48-A710-B8085D2F85C5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b83fa9e902eb627e66e02941d9af62202b0ea451","datavalue":{"value":"10.1016/S0168-0072(98)00026-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1302302$53E58DAB-DB20-4A7F-9ED3-E68A9BD4CFCF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ec91c84374e1970ffeb850b5b07163b4a998968b","datavalue":{"value":{"entity-type":"item","numeric-id":167059,"id":"Q167059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$B4D2F639-86C4-471D-B04E-D24CA23F2ED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"53993ae6db4350dacb1d3d4f5370b18b73e58da6","datavalue":{"value":{"entity-type":"item","numeric-id":167060,"id":"Q167060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$453418EE-F8B2-49FE-9ED8-86138BA4261F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$D9B3D304-D2C3-4567-8A70-FD80CB781745","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6bc2311a1e4c7e0048fc3ed2a563730637474b4d","datavalue":{"value":{"time":"+2000-07-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1302302$E4A41E86-540A-43DF-8A7D-EEAA4F3F48F6","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d9ffc5733513ce37e994da1ef6dc26bf189d4be8","datavalue":{"value":"Cut-elimination in first-order logic is known to have a non-elementary complexity. The authors investigate ``reduction classes'' \\(K\\) for cuts [cuts over formulas \\(\\notin K\\) can be feasibly eliminated or replaced by cut-formulas in \\(K]\\) and for cut-elimination [if all cut formulas are in \\(K\\) then all cuts can be feasibly eliminated]. For \\(K=\\text{NNF}\\) (negative normal form: no implication, and negations are applied only to atomic formulas) every cut is easily reduced to a formula in \\(K\\), and hence cut-elimination for \\(K\\) is not feasible. For \\(K=\\) Prenex Normal Forms there is a quadratic transformation of a proof with arbitrary cut-formulas into a proof with cut-formulas in \\(K\\) sending derivable formulas into \\(K\\). However, elimination of new cuts introduced in this way can be non-elementary. Monotone formulas are constructed by atoms including \\(\\perp\\) by \\(\\forall,\\exists,\\&,\\vee\\). The authors prove that the elimination of non-monotone cuts has non-elementary complexity in the worst case. First, all monotone cuts are proved to be quickly (almost exponentially) eliminable from proofs of quasi-monotone formulas. Then it is noticed that Statman's sequence of equational sequents with no Kalmar-elementary bound for cut-elimination can be encoded by quasi-monotone formulas. The long proof of quick cut-elimination in the paper can be simplified using two observations. Statman's sequence is encoded by Horn formulas, and pruning transformations (underlying Harrop's theorem) allow drastically ``skolemize'' monotone formulas proved from universal Horn axioms.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1302302$CD777F9E-7E6A-4F2A-A9D7-0FC7F80BFACE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1302302$F30140CA-F53F-4CAA-BE5A-10DF5F0DA951","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1302302$BA82B025-75E8-4F45-B984-4458F9A91648","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"63398b314f0e2e1a67715bd60df1f0b7f414b762","datavalue":{"value":"1340820","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1302302$1D897D18-BE2A-4945-B788-54B50FB6A47F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eca72038a57a840dbce403c6e64b7914e73751a9","datavalue":{"value":"cut normal forms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1302302$55015B89-CBC0-495A-8247-EB5FD1EA6931","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1302302$3432AB84-01E0-4A98-A2E6-23F15021CAF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0f93d9a75a1caf8fa1cbb339122c6fe63132b08","datavalue":{"value":"non-monotone cuts","type":"string"},"datatype":"string"},"type":"statement","id":"Q1302302$15DA792B-8326-452A-B847-D8A95AA49A3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"89f2f833b3ab8d994fc4522eb974d4dccf12ad0d","datavalue":{"value":"non-elementary complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1302302$883BB817-B2AE-4F49-9263-CB719105E218","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ede320c64512236be213e38a2c6863b9fa3b4ba","datavalue":{"value":"equational sequents","type":"string"},"datatype":"string"},"type":"statement","id":"Q1302302$015AAF5B-7B3D-4F2B-A50A-57AF23429C19","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$A78D7855-93BE-4A83-80AC-09E3893013F6","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":"Q1302302$69EF1A87-0553-4934-82D9-C28B0A0FDE5F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b559e594edc07777117cb084e905ea94187a1df3","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$68AF6DF0-CD73-42EF-9956-B37D9C80B91A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3307606e4ca2c512b1266e827d870bcdfddae98","datavalue":{"value":{"entity-type":"item","numeric-id":4362908,"id":"Q4362908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$344EB43B-68FF-4416-A52E-514180A3E537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fd06fe8727e317c06fb69269e2a9e284cfb2205","datavalue":{"value":{"entity-type":"item","numeric-id":3882443,"id":"Q3882443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$30C69502-D4AC-4A3B-A018-FA676962A6BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86e2b29d9b4dadfb2f5b72715f7422f8e108a4ff","datavalue":{"value":{"entity-type":"item","numeric-id":1167721,"id":"Q1167721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$D862394F-E3A1-498F-86DF-3F3C090C5BBA","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":"Q1302302$2B8068C6-6E6B-45B7-8A80-8A71ED114EF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1813c495b4019dbc5a0338bf865711982b775489","datavalue":{"value":{"entity-type":"item","numeric-id":4198750,"id":"Q4198750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$5534CA5D-76A6-41F9-AA2F-E985F2A7382D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1302302$4122BA62-D2BD-4C2D-A72D-6CB5E8703A75","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"397e9aa2e88d0b60f5c997965e68607b50439e2b","datavalue":{"value":{"entity-type":"item","numeric-id":4453638,"id":"Q4453638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2862932ce1450336d3b94fdbc4a0f718419bb12d","datavalue":{"value":{"amount":"+0.8679723143577576","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":"Q1302302$59F15CDF-E94A-4C41-AAA0-F32C12FD2118","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":"ed3368962a9b78d43c8137088c2fa2d6e0bf1ce4","datavalue":{"value":{"amount":"+0.8137227296829224","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":"Q1302302$744747E3-6F1A-4837-A7B9-16D96795BFE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9584f1ec64749e9f2a9214f5a86f967961523480","datavalue":{"value":{"entity-type":"item","numeric-id":4436026,"id":"Q4436026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d97f6c04a22e83f71c31c69b97a8f6ab20ae1d8","datavalue":{"value":{"amount":"+0.785655677318573","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":"Q1302302$84CBF3BF-11F5-40C1-A004-DCF4752FC5E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7a03b82fa18111f7f043489b71fd32ab33840af0","datavalue":{"value":{"entity-type":"item","numeric-id":650922,"id":"Q650922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3341157371a9e6690b2775287df9e99e04d0bac","datavalue":{"value":{"amount":"+0.7843664884567261","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":"Q1302302$2CF64D2E-CFD1-45BD-818C-1A990DD3085B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae76515d6348a1777aba34e5d6a5bf8225d7ec00","datavalue":{"value":{"entity-type":"item","numeric-id":402115,"id":"Q402115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9240417ac38e8e1a02410af1308ad5424333f041","datavalue":{"value":{"amount":"+0.7787602543830872","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":"Q1302302$65DD962F-0B5A-4AC5-8202-55445C7F44E6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut normal forms and proof complexity","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cut_normal_forms_and_proof_complexity"}}}}}