{"entities":{"Q920967":{"pageid":922815,"ns":120,"title":"Item:Q920967","lastrevid":49417696,"modified":"2026-01-07T03:14:04Z","type":"item","id":"Q920967","labels":{"en":{"language":"en","value":"Resolution proofs of generalized pigeonhole principles"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4164797"}},"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":"Q920967$11FB39F0-B815-4410-9C8E-DC2BBA9B2C13","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3298b0847b93b9797cef7d1b00ebc7f439014666","datavalue":{"value":{"text":"Resolution proofs of generalized pigeonhole principles","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q920967$467878E4-DF76-49F1-956B-DA75A7A85215","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"205bbbe4598187cc8ac306af2cd88c84a024de2c","datavalue":{"value":"0709.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$CF16B36C-C299-4309-BE2B-95D762B233D1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"832564728548a002a9b2367bad0d6b01b81d12a1","datavalue":{"value":"10.1016/0304-3975(88)90072-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$7EAC5D2C-4369-43EB-B840-1657FB499C95","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"556b5f897f5d545f04c26b56d4624f5cc4b2661a","datavalue":{"value":{"entity-type":"item","numeric-id":195654,"id":"Q195654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$BB9B4EF9-2795-4787-85B6-2569AB96FA9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c66a437d74ae466cacad614cef92f8e5d71204e6","datavalue":{"value":{"entity-type":"item","numeric-id":239429,"id":"Q239429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$DDB19C38-91A3-45F3-8CF0-D2D837A64F57","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":"Q920967$4170083C-0174-4416-A24D-BCE13F2D2565","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q920967$29F96FBD-7F63-44B5-ADB9-2D97F0E6D18E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d97e8cc6d441f88232682cbd85970fd3ed11fcca","datavalue":{"value":"The generalized pigeonhole principle is that for positive integers \\(m>n\\), if m pigeons sit in n holes, then some hole contains more than one pigeon. The ordinary pigeonhole principle has \\(m=n+1\\). For a fixed m and n the authors exhibit a set \\(S_{m,n}\\) of propositional clauses which encodes the generalized pigeonhole principle. The number of clauses in this set is \\(O(nm^ 2)\\). They show that any resolution refutation of \\(S_{m,n}\\) will contain at least \\((3/2)^{n^ 2/50m}\\) steps. It follows that the size of the refutation is exponential in n if \\(m=cn\\) for a constant \\(c>1\\). This extends work of \\textit{A. Haken} [ibid. 39, 297-308 (1985; Zbl 0586.03010)], who gave a similar result for the ordinary pigeonhole principle.    In contrast, it is known (references are given in the paper) that for a large number of common propositional logic proof systems, including all Frege systems, polynomial-sized proofs are possible for the pigeonhole principle. Furthermore, it is known that all these systems are polynomially equivalent in the size of proofs they generate. That is, given a proof of length l in one of these systems, there will be a corresponding proof in any other whose length is at most p(l), where p is a polynomial. Therefore, the result of Haken shows that resolution is not polynomially equivalent to any Frege system. The authors of the present paper strengthen this by showing that there is a constant k such that resolution is not polynomially equivalent even to formula-depth k Frege systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$5BF7ABCD-358B-4217-9B21-26AA4529C97C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$D35E2DD7-0312-4529-ADDB-7E3F3DF3F09E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$745E4F30-B05F-4BDE-9574-045B72B4361F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$8ABC3994-5367-40CA-903C-C513001D8EB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$9DC74227-792D-431F-A259-8B6AFDC364FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$8F7C7171-BC05-4F20-A336-FEC78939E782","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9e6fa99c31535c63762f79bf8ca10d3899c5fb25","datavalue":{"value":"4164797","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$87BBB437-ED44-4FCC-806B-C8E10DAA01F5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7cd73047e2159e94e028e9df0a19c22f5e506d93","datavalue":{"value":"polynomial equivalence","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$9900C4F8-D7DB-44DB-AC1C-884041FBBCA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"184e4219497cffdf83c8d9d9583396b29fbcfc7f","datavalue":{"value":"generalized pigeonhole principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$8432F9E6-DEE4-4422-B641-9DC0D200D902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b4bfa67db5a3094d4b88049452c4eac336365515","datavalue":{"value":"propositional clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$ADB43B6A-3F53-4793-A97E-5F0E49294C17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e6ffb1c353cab625622161ce27f82723a019913","datavalue":{"value":"resolution refutation","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$D458A116-F06C-439A-A24D-EF1537BE22FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b67531ce85de68d1bc9749a22a779e09237c4b98","datavalue":{"value":"size of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$1DF3CF6D-03BE-44F7-AB1A-3903844287B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f7e939acf4ed91cdd39f1bd56576107c47fb06","datavalue":{"value":"Frege systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q920967$C701FAAB-2CE6-45E2-8E4C-358CD9337223","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":"Q920967$7EDA92B6-37E7-4B68-995F-F74B09A13945","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fa33b3d5dd0ab44ad681366db605894c38c90f94","datavalue":{"value":"https://doi.org/10.1016/0304-3975(88)90072-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q920967$40441F6F-1375-4C9D-A2AE-1B42B4F3E56D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8a2d2ba1a8b56cb4c4775a04f667c5e646c55cdf","datavalue":{"value":"W2062912795","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q920967$85CF793B-7770-4F3A-8371-EACA76AEB820","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f31cbeafb74eb2331031a6d2305fa02411af3e7","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$748B2B16-12E3-4874-BA70-A9D06761B622","rank":"normal"},{"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":"Q920967$D3F692CD-E4DF-451A-A2DB-5DC0AC6938CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cebc572d627a83eaa191f68127ff59e387905680","datavalue":{"value":{"entity-type":"item","numeric-id":580175,"id":"Q580175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$D8048F5C-7BE6-42ED-980F-C5AA07EA819D","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":"Q920967$B8897AC7-BB4B-4D17-9195-A32D1C505B43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85c91a2d52fb100925548482e5c1cd7bcae9e61d","datavalue":{"value":{"entity-type":"item","numeric-id":3689182,"id":"Q3689182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$FD3DC32C-26EE-4111-91CD-432A6D5298D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a3b936472256c474ab8250b72e7c010873198894","datavalue":{"value":{"entity-type":"item","numeric-id":4206725,"id":"Q4206725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$013C5413-583C-4191-A789-5314AED9FA0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q920967$507E609B-35B8-49AC-9379-6B77DDA28E76","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c2cccaac9b36deb25402bd0f6ccff787ac830afb","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1676e596678a658b369f779020802cfe806d70f4","datavalue":{"value":{"amount":"+0.8724134564399719","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":"Q920967$90DF46E6-B6D7-4401-89D2-A513AC5F2C0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80adba55132ad81c69da414cbebaa257ccfb28de","datavalue":{"value":{"entity-type":"item","numeric-id":5501187,"id":"Q5501187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5a29443514e6c4b6af701ab045b2af5a5296cc0","datavalue":{"value":{"amount":"+0.8652029633522034","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":"Q920967$B46D8768-29D9-4DDB-918C-BF1444FA5160","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b8619ab5791ecf083dffaaaa18e3233c03cbac4","datavalue":{"value":{"entity-type":"item","numeric-id":4847394,"id":"Q4847394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2804876d69e360903e281068aa7b5630ef4ca858","datavalue":{"value":{"amount":"+0.8551757335662842","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":"Q920967$2BF72F8A-7C09-47A2-B4A0-38C842D3BA0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86bb30c857885d253bf26bca70742f428e38536d","datavalue":{"value":{"entity-type":"item","numeric-id":5898862,"id":"Q5898862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26a21975b5f3b2c1d719aada3ac537647da20bca","datavalue":{"value":{"amount":"+0.853959858417511","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":"Q920967$D3DAA069-C3A2-42FD-87EE-982B5968A4A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69cf90495e95ccafed6b110166466fb6ca23310d","datavalue":{"value":{"entity-type":"item","numeric-id":1401365,"id":"Q1401365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"564c75ab32e27a289ea5e536c8abca820c436a3f","datavalue":{"value":{"amount":"+0.8533284664154053","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":"Q920967$03295CA0-B6A3-40B2-906F-91E3BDDBF700","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:920967","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:920967"}}}}}