{"entities":{"Q1575658":{"pageid":1586398,"ns":120,"title":"Item:Q1575658","lastrevid":74064819,"modified":"2026-04-14T18:14:19Z","type":"item","id":"Q1575658","labels":{"en":{"language":"en","value":"The proof complexity of analytic and clausal tableaux"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1493447"}},"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":"Q1575658$98C2DEC8-722D-4251-956E-2200D0BAF118","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e40d200dbc189d08e49302433bd76edccec58630","datavalue":{"value":{"text":"The proof complexity of analytic and clausal tableaux","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1575658$52CBBA16-40A6-451F-8F41-978264688A8E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"43fc776d7f1198ac6509611aca0dec2b24cdffa7","datavalue":{"value":"0947.68130","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$BE7CBBF0-9560-4B31-8535-7B70EC61E3D4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7ba03f81177ca4c0261adfda56764921a46e7216","datavalue":{"value":"10.1016/S0304-3975(00)00148-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$57AFAB5E-CE47-4B3F-B7F7-295FC0406CE0","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":"Q1575658$97313098-7998-40C7-8F4E-0B1D7D16CBB6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b3a497233c3b9babc42d370358782cbff338a7a1","datavalue":{"value":{"time":"+2000-08-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1575658$873D9127-767A-4B6F-896A-66B4919CD1DA","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"99721464ff9491a7449f4e4cb32a59bc12472d75","datavalue":{"value":"It is widely believed that a family \\(\\Sigma_{n}\\) of unsatisfiable formulae proposed by \\textit{S. Cook} and \\textit{R. Reckhow} in their landmark paper [Proc. 6th ann. ACM Symp. Theory Comput., Seattle 1974, 135-148 (1974; Zbl 0375.02004)] can be used to give a lower bound of \\(2^{\\Omega(2^{n})}\\) on the proof size with analytic tableaux. This claim plays a key role in the proof that tableaux cannot polynomially simulate tree resolution. We exhibit an analytic tableau proof for \\(\\Sigma_{n}\\) for whose size we prove an upper bound of \\(O(2^{n^{2}})\\), which, although not polynomial in the size \\(O(2^{n})\\) of the input formula, is exponentially shorter than the claimed lower bound. An analysis of the proofs published in the literature reveals that the pitfall is the blurring of \\(n\\)-ary (clausal) and binary versions of tableaux. A consequence of this analysis is that a second widely held belief falls too: clausal tableaux are not just a more efficient notational variant of analytic tableaux for formulae in clausal normal form. Indeed clausal tableaux (and thus model elimination without lemmaizing) cannot polynomially simulate analytic tableaux.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1575658$6123C145-8EB0-4C54-9C71-4B8692F48780","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$F9638549-B339-4B7B-AAB8-F4E66B1AC159","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$7D89E382-7159-465B-BFCF-77B83D8325F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$4758D694-D6E7-4632-87FE-887874876C7F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ec96db703f8cb7c234145ee62526321ed1f4ed1f","datavalue":{"value":"1493447","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$A106F301-8F85-4D5A-9958-7054ACAF8553","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e269374e5a98e44a2949e7e46023a94d0f33df27","datavalue":{"value":"analytic tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q1575658$C84A4744-E6D9-455D-BEEF-74AF5EBBF9D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1575658$DC8A3AF3-8A72-44A2-93F9-CBDE08988E58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b36f00d71c56e77d79dde339ed1cd537cf241d9","datavalue":{"value":"clausal tableaux","type":"string"},"datatype":"string"},"type":"statement","id":"Q1575658$2B4039BD-9182-4EDE-9BAE-3CDF5386D6E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1575658$13FD61BC-ACA2-4600-935F-54FD182D9A47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d8528a6280cd0e6cc6c4c3d14fe349c6e82a2d3b","datavalue":{"value":"tree resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1575658$2E12144C-0CAA-4C43-9A24-7F5FC8DA75F6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd8358f34fdd94323fe17d3e8928b2b07a4e9975","datavalue":{"value":{"entity-type":"item","numeric-id":861697,"id":"Q861697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$EEEF2269-85FA-4246-8408-300AF8302979","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":"Q1575658$628DD830-A0FB-4F6E-A196-12877629A61E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7273ec0eb958a68acc1c78fd022c2a6c6886f422","datavalue":{"value":{"entity-type":"item","numeric-id":1350509,"id":"Q1350509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$46B14FD4-0A5C-4DFF-BC16-46A5CD0E16DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df4b2cc45597c6adb320160f2d26e8212e854497","datavalue":{"value":{"entity-type":"item","numeric-id":5235250,"id":"Q5235250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$BDEE626C-C294-40DD-826C-97C1991655BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81494301ed40478ad47563138f01784b63003971","datavalue":{"value":{"entity-type":"item","numeric-id":4152212,"id":"Q4152212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$39B0F7BF-259C-410C-BF6E-567367752534","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":"Q1575658$B039E98E-D5D1-4B1C-89A7-C3DECFA03FC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b19a13d21f909bc5d01ac054faba1d283210dbc5","datavalue":{"value":{"entity-type":"item","numeric-id":4304496,"id":"Q4304496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$EE96FE8B-4854-4AAE-9D9D-4A2E5962637A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"158bb2233935470152d2dc667c5dec4b7a43c81a","datavalue":{"value":{"entity-type":"item","numeric-id":1344875,"id":"Q1344875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$4E1B038F-39A4-48D6-8C6D-F1DCF4F19564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65f72fa731d5ef46f7c8727b7b59f2eaf22c3523","datavalue":{"value":{"entity-type":"item","numeric-id":5544307,"id":"Q5544307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$7186E071-6E8F-4D18-8B18-B9233661D023","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e871f7502e5ca1ca7c6fbeffba5e26e186a53d96","datavalue":{"value":{"entity-type":"item","numeric-id":4318171,"id":"Q4318171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$7A0F3D02-9323-4B9E-91CE-194D1CB9DAA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb4ba955596cba8022ed29b088e14f54735c943","datavalue":{"value":{"entity-type":"item","numeric-id":1331929,"id":"Q1331929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$ACC9845A-9DDA-4188-B5E5-963725D0B50F","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":"Q1575658$20C3CBDB-33B1-4F44-B9A5-74BC1C2E3356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"febba330446bda559f2952d624c63d67c91597ef","datavalue":{"value":{"entity-type":"item","numeric-id":5560258,"id":"Q5560258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$914D35B9-8223-4E4C-A5D2-F1FF8D97D8B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acddcbbc7bbb65cd6789ce6d861571f4cbd168d8","datavalue":{"value":{"entity-type":"item","numeric-id":4873893,"id":"Q4873893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1575658$05D680DF-097A-4D0A-89F3-CF91D01B89A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"524d4cafa735a8a66b877d8529aff486f203347f","datavalue":{"value":"https://doi.org/10.1016/s0304-3975(00)00148-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1575658$72CFB052-ED79-45C7-91FC-603555492B99","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b44fd9533d1d7b6057d38c4901838a9e7ef1eee8","datavalue":{"value":"W2120887282","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$8714C30A-4684-47D1-B0B1-D870FB5FF2B1","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"684022aa0d9f17c0407efff58485f3aca995a304","datavalue":{"value":"Q127482007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1575658$1A15253E-1C29-4656-BD79-7C23739FAE3E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08680def47457321ceda7f1220ccfebb6a1a62f5","datavalue":{"value":{"entity-type":"item","numeric-id":3410672,"id":"Q3410672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c4d85db45892b799ec5423d1fee3ac688887e1e8","datavalue":{"value":{"amount":"+0.8841260075569153","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":"Q1575658$F0D3FBD7-4F7E-4B5C-A4F5-4E64D0BEE914","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"90da4d6e7f8c4b5d2db00c0f177c40e4486aef67","datavalue":{"value":{"entity-type":"item","numeric-id":5175990,"id":"Q5175990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae84013b07c4e7ae62a86a54525858e253c0df4d","datavalue":{"value":{"amount":"+0.8680678606033325","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":"Q1575658$DAD31524-1A9D-4836-9F86-EE91419D0547","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57a803d379bbf3135ca6388d0053cc626dfbca1e","datavalue":{"value":{"entity-type":"item","numeric-id":1314288,"id":"Q1314288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4d9cd33262dd98b0560207f1db328cafabe7d51","datavalue":{"value":{"amount":"+0.7972875237464905","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":"Q1575658$BE94FF6E-5955-460B-9543-C0C75491412B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bcc652cfc22b112710f16eea100413b4946b669a","datavalue":{"value":{"entity-type":"item","numeric-id":4318171,"id":"Q4318171"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56b23b8028b6c331a1f2b8313a2d4dd95e64f57d","datavalue":{"value":{"amount":"+0.7954559326171875","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":"Q1575658$CEB617D3-C7B2-4D65-9D84-AAF51BD4221C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The proof complexity of analytic and clausal tableaux","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_proof_complexity_of_analytic_and_clausal_tableaux"}}}}}