{"entities":{"Q3088019":{"pageid":3098734,"ns":120,"title":"Item:Q3088019","lastrevid":86175032,"modified":"2026-06-03T15:47:49Z","type":"item","id":"Q3088019","labels":{"en":{"language":"en","value":"LCF-style bit-blasting in HOL4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5940079"}},"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":"Q3088019$34D7F16D-85EB-4549-A6C7-D091D0D1B7D6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d1c4c329bd1588451f991d0b74f4bf20348f7c47","datavalue":{"value":{"text":"LCF-Style Bit-Blasting in HOL4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3088019$C8165703-60F3-4BB4-98D7-3A383DAE8EED","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ac7f41fdd0ccfd27dd76f6472e6418fcf6100fb6","datavalue":{"value":"1342.68283","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088019$E26B4093-3755-41A3-AE67-73168B25B091","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"10974a61a4cb71f8ea09168511f168fc8b8d8e50","datavalue":{"value":"10.1007/978-3-642-22863-6_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088019$536E7117-A0A0-424A-9A26-0A123224D331","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"30e84c1c161a78deee54f35997c4f862ecf81aa5","datavalue":{"value":{"entity-type":"item","numeric-id":172359,"id":"Q172359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$0BA36F87-70C5-472B-896D-50F46E03E3A3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$99A0C7A5-21FB-4254-95E3-5D0F7B067769","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cf253edeced6fad2edf52e73f99001914b4fc105","datavalue":{"value":{"time":"+2011-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3088019$5B93715B-AB98-4CAC-9AA0-B5E7641DDCE4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088019$88B9A13B-1519-4A9F-BAA3-EB27859FE780","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1b100222e3a6af1936f06821bbb405d6d85e2fe7","datavalue":{"value":"5940079","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088019$BF17C703-3AB3-4748-9FD5-83224C6A01BD","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$4EB90096-09EC-47CC-948D-80798F7FD046","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$582BF246-A72E-44A8-98F3-148A819B648F","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":"Q3088019$11C45D48-E182-4E97-93F4-06E7100C92F5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2891effe248e80a546618225c0f40cf6f114314b","datavalue":{"value":"https://doi.org/10.1007/978-3-642-22863-6_26","type":"string"},"datatype":"url"},"type":"statement","id":"Q3088019$78394ABF-8621-41E2-AC5F-CC99EB9281EB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"21489ab8eef0010a49033793f48c5b67b625ec88","datavalue":{"value":"W2165236431","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3088019$4BCFAC52-C7B6-4D1F-B457-80650E89391F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$8AE72940-E26A-4240-92BE-315D13FA8513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"494aa31720bff090f87eabeb86ce7380ba058cbf","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$B10B2543-FE88-437B-8B0C-9395A3E80D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69fc57724798b1f4f5d16b3ee29953bbaadefc63","datavalue":{"value":{"entity-type":"item","numeric-id":5758122,"id":"Q5758122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$DCDBE0C7-A315-4936-BA8D-2DEAA5F9CB1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$E3E1AADE-331E-4C11-803D-5274C8D00794","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9990a2e16f4d96fb2dc6e7fcff54427a1d73f706","datavalue":{"value":{"entity-type":"item","numeric-id":3088011,"id":"Q3088011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3088019$6BF5950C-14D6-4CFB-9964-F2F16F175A84","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba3d44bbd36b0708161e2ec3ff7b4197443a7cb0","datavalue":{"value":{"entity-type":"item","numeric-id":3100212,"id":"Q3100212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ac46cad0ecbf3cfff64d0186069bcc32e90107c","datavalue":{"value":{"amount":"+0.79438316822052","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":"Q3088019$38358807-CA73-458C-BBAB-2B11BB027998","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1911663a64677dd41e915eba33d6d9370e47ba6a","datavalue":{"value":{"entity-type":"item","numeric-id":2181940,"id":"Q2181940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"504431ecff3d0f311b1ecd5552cfc5b16c11a73e","datavalue":{"value":{"amount":"+0.7660568952560425","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":"Q3088019$C7A6D4F2-0212-4774-ABB9-1B2E7E7061E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d13a1aa7335cec291b0dfd74d25004b6bcf26c1d","datavalue":{"value":{"entity-type":"item","numeric-id":3460065,"id":"Q3460065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b36b73c415201e63afdc79a1c476fa09b2896357","datavalue":{"value":{"amount":"+0.739128053188324","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":"Q3088019$4BDBA60C-72E4-48AF-82BF-982EC0EC9FFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"887925069d9615572d47c7b054d26f8f6ec28e24","datavalue":{"value":{"entity-type":"item","numeric-id":5758122,"id":"Q5758122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d359a5d59609eeab24846dfae5c87ad2e6c8aa4","datavalue":{"value":{"amount":"+0.736861526966095","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":"Q3088019$7D0C3DCC-37F9-459E-9E41-FDB12622850B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59b7b179af91ff79850e6500bf44206f23fadf51","datavalue":{"value":{"entity-type":"item","numeric-id":2815126,"id":"Q2815126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a4d24847f4f4e6449ceb67d41178ff3600e159b","datavalue":{"value":{"amount":"+0.725948691368103","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":"Q3088019$06EBA59D-546B-4883-8D43-2DCAF391988F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"LCF-style bit-blasting in HOL4","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/LCF-style_bit-blasting_in_HOL4"}}}}}