{"entities":{"Q5402611":{"pageid":7432185,"ns":120,"title":"Item:Q5402611","lastrevid":74432592,"modified":"2026-04-14T22:20:03Z","type":"item","id":"Q5402611","labels":{"en":{"language":"en","value":"On the computational complexity of finding hard tautologies"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6270262"}},"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":"Q5402611$553FAE49-7042-47E1-AAD8-7963CAA8E284","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1d7664e9741191f5f2d30fcd56c4377f94bb4d59","datavalue":{"value":{"text":"On the computational complexity of finding hard tautologies","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5402611$F2D7D5FB-ACB3-4D23-8066-1A9C0585B4D6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a4bf09cf3c8656a3d03971d4d36f9e79b42d6421","datavalue":{"value":"1345.03107","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5402611$D388DC65-4935-44D8-9079-7BA86F7A2882","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e4b9ae896fbf78b3fa2084fd5300754d74076f66","datavalue":{"value":{"entity-type":"item","numeric-id":226860,"id":"Q226860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5402611$7B09F6F8-25A9-4B41-9EFC-CB27EAC096C2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"01b7f37608d9f87bfa2998bb736dc8e29f05f57a","datavalue":{"value":{"entity-type":"item","numeric-id":2759195,"id":"Q2759195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5402611$899CF5C8-496D-4228-A1A9-9500F5A23138","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b43a2c2b6eb630f564616ba070a6751b081d8977","datavalue":{"value":{"time":"+2014-03-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5402611$AACB2354-8A69-4CCC-A36C-D9697B635749","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1e4465df81b061c12f2dd4404a450e67f30a51b9","datavalue":{"value":"https://arxiv.org/abs/1212.1789","type":"string"},"datatype":"url"},"type":"statement","id":"Q5402611$F756E062-7D32-4B5C-AB1E-1DE60C7CA07C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5402611$B89471F1-98CB-40C8-A12F-1DA1570359FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b4346faa01bb5fb0576370374d6456afd58d5666","datavalue":{"value":"68Q15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5402611$BAE14580-9AFA-4C80-8AC2-B2C67CB76C26","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1489a06396753e03dfc0bc79e2ebe5d89fb6c008","datavalue":{"value":"6270262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5402611$B622F696-9E75-4597-B470-5550E68AA19F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b24e51e460d663f6ecf18860b761adb8bb29e572","datavalue":{"value":"propositional proof systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5402611$0232C5D6-3BD4-4BAD-B9A0-D9475D021507","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"986e975208b070c5142b42b7967bb38dc4fad0f4","datavalue":{"value":"proof complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5402611$0C3E6216-21F6-4D8C-97A4-3B9027E6E19F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ca725f8dc0ee223878b2f92392adf9d958dc571","datavalue":{"value":"Nisan-Wigderson generator","type":"string"},"datatype":"string"},"type":"statement","id":"Q5402611$85E5A932-29BD-4B45-8307-A5275FFE30A5","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":"Q5402611$49AA92BD-3529-4479-92DA-DD25B838C8C8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c574630bf614825f677fe90c49944044f0dc13eb","datavalue":{"value":"W2106792056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5402611$2FD2AE30-F93F-4368-81AB-B41CB07BCE63","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e558dbadaa9bd63e072ed73075ff642846ea2417","datavalue":{"value":"10.1112/BLMS/BDT071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5402611$BEE2D216-4E9E-42C8-9814-81BD38ABD983","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49f87d27cf30154a785f3bdc83eb61577b1aa955","datavalue":{"value":{"entity-type":"item","numeric-id":5957903,"id":"Q5957903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9242d427ec7eb10309e38e217180fd06fb28c428","datavalue":{"value":{"amount":"+0.92007446","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$4ED68CF9-64F6-4571-B6AD-BCAF9B06007C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"570af33c65e718ba3100773cbecfd2b03fd090b4","datavalue":{"value":{"entity-type":"item","numeric-id":4501542,"id":"Q4501542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32529b774b26e9338861ec3def4bd1dc85f35b61","datavalue":{"value":{"amount":"+0.9055534","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$CBFDDD84-153D-45D7-9C3F-CC7041111DB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e3a8e0e6322df6f8ed359156af105a91bb5ef33","datavalue":{"value":{"entity-type":"item","numeric-id":4364539,"id":"Q4364539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"827eacd57614447fe0049f26c18552c315613c6f","datavalue":{"value":{"amount":"+0.9033018","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$73EF532C-B599-4978-9F2A-4BECCE6C9EB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92979ab8e0586da2f4576edf8877ec60b7924fc4","datavalue":{"value":{"entity-type":"item","numeric-id":4375783,"id":"Q4375783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1c9f36c9a6ef935a4bb4ee4f69745dc0d1f7cfd","datavalue":{"value":{"amount":"+0.89312494","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$80068F89-C286-48F0-B8E7-832B59C5B24A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3c6658152736335139678d1ea048bf037942bb5","datavalue":{"value":{"entity-type":"item","numeric-id":3724328,"id":"Q3724328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6bebd83af84086c56845c0dd3e8edced1685443","datavalue":{"value":{"amount":"+0.8795669","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$D3187452-8F80-410F-9540-BDCE8070E669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"02e55b61410f38e6a1b24aaa79cfee91f308ed35","datavalue":{"value":{"entity-type":"item","numeric-id":4934563,"id":"Q4934563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"335d20c24c54f4d739ddc1c77dfdd41709517406","datavalue":{"value":{"amount":"+0.87832856","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$26686A62-AE81-4038-93B4-CAFC852C2E27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"96dc708fbd1384cb0999928a24e57600bbe45be5","datavalue":{"value":{"entity-type":"item","numeric-id":5593816,"id":"Q5593816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cfcd2f46d9feaea6b76e4842527af3bed18fd0c","datavalue":{"value":{"amount":"+0.87782836","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$EF827CEB-AB66-4351-9BEC-933DF17B8830","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbbb79cd512d5b3cabb96d86f48bc3ec2154cad7","datavalue":{"value":{"entity-type":"item","numeric-id":4809504,"id":"Q4809504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e1097290daae89d612cbdfad6c7603d22dd71e0","datavalue":{"value":{"amount":"+0.87642926","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$F3456615-9A11-40F1-AA49-8198F00E83EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8610d660f16a92d1153e7a3d9ccfb80ca2679f08","datavalue":{"value":{"entity-type":"item","numeric-id":4713865,"id":"Q4713865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5079035311e8d20cd39e7622789ba19f1628a15","datavalue":{"value":{"amount":"+0.87557125","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$80A19351-65C3-4AF4-BE17-A155036CA441","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f385a5a7f5f95aa3a780c4c5cf0468609549533c","datavalue":{"value":{"entity-type":"item","numeric-id":2388429,"id":"Q2388429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e49d5c626086b10efd49a834bfeac2ab5b0fc8f5","datavalue":{"value":{"amount":"+0.87354624","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5402611$5D8B83E1-A943-4778-B0D6-8ADB925C97E9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the computational complexity of finding hard tautologies","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_computational_complexity_of_finding_hard_tautologies"}}}}}