{"entities":{"Q689298":{"pageid":691147,"ns":120,"title":"Item:Q689298","lastrevid":63499272,"modified":"2026-04-11T13:34:32Z","type":"item","id":"Q689298","labels":{"en":{"language":"en","value":"Cut formulas in propositional logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 445061"}},"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":"Q689298$ECAAA8B5-A16E-41F8-9AF1-95EC70806FB5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7064c3a04c75dcc436fb6b6068a7397a8e4c81eb","datavalue":{"value":{"text":"Cut formulas in propositional logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q689298$A5F3DB57-099D-494D-882E-0810F2797AD4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ec3ce151e997ffbb77aee97f861378c54002a7a1","datavalue":{"value":"0788.03069","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$2484A132-8307-411C-86B1-655E822AD754","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d02eb3caa5d0ac01eab4f02b02be15450c5f7a03","datavalue":{"value":"10.1016/0304-3975(93)90249-S","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$97F279F0-7E4D-4FD0-96E2-C4BBCC671F3D","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":"Q689298$0CB3DAA8-A749-43EF-AF96-657296627B30","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"92112234a474f78049341bfb55637019f67e54ac","datavalue":{"value":{"time":"+1993-12-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q689298$396D92A1-8ED4-43F2-996A-D83B5060DB7F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7fa3e3bb539006693bcd2938a969b20699cd4dda","datavalue":{"value":"Cut formulas in propositional logic can speed up some proofs exponentially (a cut-free system is used as reference when we talk about speed-ups); it is hence important to study proof systems with cut, types of cut formulas (atomic cuts versus general cuts) and also relations between cut and techniques which may speed up proofs. In Section 2, we try to explain the importance of atomic cut formulas. We study the resolution principle and analysis trees with atomic cut and conjecture that there are proofs by analysis trees with atomic cuts and refutations by resolution such that transferring them to cut-free proofs will cause exponential increase of the proof length. We also study unit resolution and conclude that transferring refutations by unit resolution to cut-free proofs does not cause exponential increase of the proof length. In Section 3, we discuss using definitions in analysis trees and in resolution. We conclude that it corresponds to using abbreviations in analysis trees and to adding possibilities to use more complicated cut formulas in resolution.","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$E1AFA149-4F64-478F-AC87-22884B5EA6BB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$5DF65815-D843-4913-9CB7-31E95C61CDFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$63717003-B494-4C19-A9F2-43E2F203FAF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$3F95CDB5-3132-4B84-AE4B-6571A02480E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1c9b31a41927cf606acc07a8eff97b20245fd995","datavalue":{"value":"445061","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$33850FCF-CF93-4E89-8054-58BD6FB13CC9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93c047fb19c5161b32c5245d5c8c28b4500157fe","datavalue":{"value":"propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$70F0189C-A856-4D92-8AFA-DAC6AA250EC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22026358cc1d84f975e38349b0b466a37c9983d2","datavalue":{"value":"speed up","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$21C015F5-9622-4FE0-9840-1D70BF078B4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c944089ebd99d6195538b901db0229fcb390018b","datavalue":{"value":"resolution principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$043A240A-B202-45AE-8CA9-92CC54EDE6AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08917ae9147b582886898025eb3129ba68c5dc85","datavalue":{"value":"analysis trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$6F551170-55FD-4545-BB86-5E0B313351DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"604a3bb20470259b56d952b048fe691271dd4dbb","datavalue":{"value":"atomic cut","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$68CEEB84-639A-436B-8280-ED29FD0F54C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6bd34074526ff9d5d53722d72ef57f42fa801ea2","datavalue":{"value":"cut-free proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$121102BF-0384-4895-A22F-C4E3C210C26E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7edadeef8bb2338ff3a07e14bdbe112375679df2","datavalue":{"value":"proof length","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$B9C3014D-4BE1-47AE-900B-8CD5A3117948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07a20c0cd46b1270eaa68d6af79089b4560ac705","datavalue":{"value":"cut formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q689298$B90A6E91-EF74-4F07-93F7-08228C8EBD03","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":"Q689298$E1A2AB75-7F49-4BCC-A1DA-B07249EAD8C3","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":"Q689298$4F8D7A25-F859-458B-AF4E-A3DA7437BD8B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bea75da9fa67a5f77faa9362cd4aa6c737c792a","datavalue":{"value":{"entity-type":"item","numeric-id":4194955,"id":"Q4194955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689298$0625759D-F64B-4866-8493-179BB5EBA61E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689298$49F6BAED-0B60-4376-83FC-6219F201EB29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689298$4C1D0AAB-1690-49D7-B5A1-D7FA79EFF8D8","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":"Q689298$6F08C548-F06C-43A0-B2FA-8114F7237E0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"761227e28ec3092e559c7874757d0ce5e8b995d8","datavalue":{"value":{"entity-type":"item","numeric-id":4198749,"id":"Q4198749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689298$3C7EC817-B75F-4DF2-A513-7A29A44F0283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37e8246186317a12728382bda44d4fa806440e38","datavalue":{"value":{"entity-type":"item","numeric-id":1183598,"id":"Q1183598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689298$27C65660-4E66-4D8C-ACCD-7A0FE2FF4DA0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"114bd817c4df97cb386b6ca2f8ed01dc7cb90608","datavalue":{"value":"https://doi.org/10.1016/0304-3975(93)90249-s","type":"string"},"datatype":"url"},"type":"statement","id":"Q689298$8AC6665A-5405-4F31-8163-6C7DE9E730AF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"be3f175d7594b77e9af0507c558a7e8caa75941c","datavalue":{"value":"W2083806359","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689298$311A3F12-18CB-412E-9942-E970485ACA29","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b042aa778c18b5ad4e08620cd0c32e0d093e5e72","datavalue":{"value":{"entity-type":"item","numeric-id":4521282,"id":"Q4521282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92bd5cda6bf4ffa37428c749b1a92e859c408e2d","datavalue":{"value":{"amount":"+0.8008491396903992","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":"Q689298$8691FFA8-12EA-4EAA-9579-B1811B9D5E6E","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":"f375ae4a79a4a3a2b217dd4951be3f83820286ed","datavalue":{"value":{"amount":"+0.7779900431632996","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":"Q689298$7A54AB88-574D-4D64-8EAF-AF88C10EFA30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7cf88362f6428d5d0299f9f394699d6f8456b3bb","datavalue":{"value":{"entity-type":"item","numeric-id":2368983,"id":"Q2368983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60efbba72eb10a8ae66be4dc39b94e70d72567cd","datavalue":{"value":{"amount":"+0.7750020623207092","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":"Q689298$CAD8FF2A-376C-4FC4-9D28-62C64ED0C7EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86f03f236bca73a7a1f1ff66f7ba7911a4c07a58","datavalue":{"value":{"entity-type":"item","numeric-id":1183598,"id":"Q1183598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd5dc26dbfcadcec6995aca44eba3f041558ab67","datavalue":{"value":{"amount":"+0.7636262774467468","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":"Q689298$7903D345-229F-412A-8888-06294192EAA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54d10821cbdfa5132d838cbf161c98e8f09b6a8e","datavalue":{"value":{"entity-type":"item","numeric-id":1577476,"id":"Q1577476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47167cb760ae903f4ec3889f63066116fb685cc4","datavalue":{"value":{"amount":"+0.7611643671989441","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":"Q689298$79A29B36-A2CE-434D-9F30-C35EAE6C8391","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut formulas in propositional logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cut_formulas_in_propositional_logic"}}}}}