{"entities":{"Q5087078":{"pageid":7116654,"ns":120,"title":"Item:Q5087078","lastrevid":91401701,"modified":"2026-06-04T23:04:38Z","type":"item","id":"Q5087078","labels":{"en":{"language":"en","value":"Shortening of proof length is elusive for theorem provers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7554699"}},"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":"Q5087078$EB657B6C-032B-4EF1-B08A-1FFA76690F4A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dbde2216352f4f70821d525462248bf3b6307508","datavalue":{"value":{"text":"Shortening of Proof Length is Elusive for Theorem Provers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5087078$296557A1-84A3-4D3B-A445-19EC2F361601","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"05dee57c42a89d74cc026911c17aa45acb9bcedf","datavalue":{"value":"1490.68291","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$1F73D6A8-B188-47A1-A0B6-62DC71690C59","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6a115ffcf36cb3cc8a94c773c806e911495475f1","datavalue":{"value":"10.1142/S0129626420500139","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$6C1432B6-5C72-46DA-AA64-31143E6EDE33","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b29e6ea9ffb450b3e0d537e8a0890ad7682c47a3","datavalue":{"value":{"entity-type":"item","numeric-id":5087077,"id":"Q5087077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$EB6F2C27-DB45-4843-9F77-F04EE1540B45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"accb1f0221ea6b057b90fd9423bbb12b2a94d5d8","datavalue":{"value":{"entity-type":"item","numeric-id":2011629,"id":"Q2011629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$BB928774-7161-4364-B41A-30BB1F02AB87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"62f4c3dfde8815e16de3f8aedd68dcd9d203569e","datavalue":{"value":{"entity-type":"item","numeric-id":256718,"id":"Q256718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$CB9124B4-A8A9-4E1F-AA28-EAACE3AB0DC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"baf65bf84a9471e07b9412f58991eb0597943057","datavalue":{"value":{"entity-type":"item","numeric-id":762483,"id":"Q762483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$3EE560FA-8DFD-4E64-863E-7B20C290BB7A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"58f994d7b74f2f9fc8df9510f9a5617f37c300ac","datavalue":{"value":{"entity-type":"item","numeric-id":2842649,"id":"Q2842649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$2A83E809-33E9-4614-A588-2F06085FD4F8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"53f271a816850f44e4911f5762419f83fae54908","datavalue":{"value":{"time":"+2022-07-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5087078$6BF3BD47-28D0-4E0B-8372-0325E877AB01","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$96BA767F-7517-432F-894B-06752BB17954","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"419d6f2b09c39920e34f63114ff159a2f0a01812","datavalue":{"value":"03B05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$5592CBC5-0C4F-4299-9A39-5123B3642E99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$32CF774A-1A79-4DAC-A3AE-474EB752176D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$94A8511B-704A-4FA7-B155-449707401718","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0d578db8d8c6f72169003bb3984c5cac8903da67","datavalue":{"value":"7554699","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$D721C465-0E2A-47EE-B205-DB7378FB2E2E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d0d82938dc577c694934677cbe49af80b51ce75","datavalue":{"value":"experimental mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5087078$E50070B7-8533-46C2-8763-7114F80B6774","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5087078$4B6F4E27-3505-4A13-8677-02FE6F374B07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bec6dac8174dd919ea6453d23e44243994d90f34","datavalue":{"value":"propositional calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5087078$DAC62B82-F111-4238-B138-34A43FC1696B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ead0f5c81911c94539d6c52fcecf360d6f4d2c7","datavalue":{"value":"trade-offs of complexity measures","type":"string"},"datatype":"string"},"type":"statement","id":"Q5087078$1D885C99-4E32-4BEF-8248-C963159FC9F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2ba0cc3f7aaac8445724ef309c9eecb57f5a563d","datavalue":{"value":"computational complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5087078$A2830E43-83FE-40ED-9F52-DFB4474F9D92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93077cc6db36e07d535db7c75a2f03eb0743cd04","datavalue":{"value":"algorithmic complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q5087078$91F801B1-93BD-479F-A6A3-2717BB93DE4E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$02798C4D-42F7-4BDE-8FA4-1644E40006D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$35EDD984-FD85-4421-ACB0-AD6502E5FE92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$84A1E0B4-3750-45B0-BDE2-B98D51CB2F5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$8F2F9DEE-BEAA-4018-B127-07932DBBF470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$D1164086-020A-43C1-8C4E-54037E953D99","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":"Q5087078$9EFC03E7-4C68-4C3A-9B0F-66DEBB901D20","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9cb2a4e4fb6a095d91ee24830284f50b193c2fb","datavalue":{"value":{"entity-type":"item","numeric-id":2732273,"id":"Q2732273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$CAF22682-488B-4876-B860-91800F59376F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61dbf611691a98c9e2b53825b06f47d0c5827bf9","datavalue":{"value":{"entity-type":"item","numeric-id":5427804,"id":"Q5427804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$B83E2825-1491-422B-A973-76E38B1F72C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f74df4601303f9c84fd6fe78b2928f4cb27f544","datavalue":{"value":{"entity-type":"item","numeric-id":1577339,"id":"Q1577339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$DB8E3B90-9188-48B6-A2FE-C06CD36FC88F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94fd9e1ae5ed1341d5e0fdd605c2d464250f728c","datavalue":{"value":{"entity-type":"item","numeric-id":2891314,"id":"Q2891314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5087078$CE6FB124-30A7-4381-A7D7-878C2CB754EF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f6fe2445360a7b1ebcae306ca1cae0c04e61505b","datavalue":{"value":"https://doi.org/10.1142/s0129626420500139","type":"string"},"datatype":"url"},"type":"statement","id":"Q5087078$D278B9A4-71CB-4DD1-A1F0-D16CEDDC3865","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8716867d599516b0257df1a1d04afdc18ebef775","datavalue":{"value":"W3120358209","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5087078$16071367-294A-4929-A085-44BBF6E29DBE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"507b3bfe8aab15501c87e7358c5f5c7db473c6f4","datavalue":{"value":{"entity-type":"item","numeric-id":4406287,"id":"Q4406287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ba47f0653944cdc847b31935fba95487a182448","datavalue":{"value":{"amount":"+0.7189748287200928","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":"Q5087078$328ED119-541E-4DFA-83B9-F42BC223D941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c70c7c6cc56bc304adf4c26e41735c161bfeeaf9","datavalue":{"value":{"entity-type":"item","numeric-id":5178991,"id":"Q5178991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"193a9f7bb9a22c7f79b2b57deab6b370f8321b5c","datavalue":{"value":{"amount":"+0.7109782099723816","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":"Q5087078$68F68B30-5DE5-4BA8-B740-C65CD5D266BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1977ce75e4c66a6e986ece8bd137815f9305537","datavalue":{"value":{"entity-type":"item","numeric-id":4345253,"id":"Q4345253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fa4fa026c017181aa79a3e300365bd67911efe4","datavalue":{"value":{"amount":"+0.7081527709960938","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":"Q5087078$AEA01705-1075-409B-9461-E81F71438750","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bedcca7522067bd4c9657d84c45f2b6bd8d3026","datavalue":{"value":{"entity-type":"item","numeric-id":1272613,"id":"Q1272613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fa4fa026c017181aa79a3e300365bd67911efe4","datavalue":{"value":{"amount":"+0.7081527709960938","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":"Q5087078$E10BEB7E-19F2-4289-8528-F930B24BB927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"84608daa68a026435a1277ea9099af93d0fc7c67","datavalue":{"value":{"entity-type":"item","numeric-id":1810853,"id":"Q1810853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9180771c70923f6dbe66ca15e967ae90de30cb9","datavalue":{"value":{"amount":"+0.7055069804191589","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":"Q5087078$6C381A26-7DA0-40A8-AE14-27C7AA2414D3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Shortening of proof length is elusive for theorem provers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Shortening_of_proof_length_is_elusive_for_theorem_provers"}}}}}