{"entities":{"Q5178883":{"pageid":7208455,"ns":120,"title":"Item:Q5178883","lastrevid":52226543,"modified":"2026-01-21T05:00:52Z","type":"item","id":"Q5178883","labels":{"en":{"language":"en","value":"Avoiding exponential explosion: generating compact verification conditions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6416242"}},"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":"Q5178883$A3060811-50C2-4DD0-B55E-6EE2EF4285B0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9ba98168d6d7ba79de87df3ec5d85ef879b8f25d","datavalue":{"value":{"text":"Avoiding exponential explosion","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5178883$D7499B7F-5239-43EB-ADE9-653539823B32","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c9ab339ab98aaad6af1d32693fd03e228f51f4b0","datavalue":{"value":"1323.68372","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$61575626-ADE3-415B-B44A-C5762B85F174","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"351d75b35f47b77ad1f286d92f0b2a13fe128d08","datavalue":{"value":"10.1145/360204.360220","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$D9A3B0D8-591B-4F7A-A3A1-B391D5705207","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"38126dc183098febb961ba3435b28eb28edd09c1","datavalue":{"value":{"entity-type":"item","numeric-id":557791,"id":"Q557791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178883$A0C2BD26-9411-4655-8D70-5FEE192AC391","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c19976f280af2a9432c2c51239959366e237e59c","datavalue":{"value":{"entity-type":"item","numeric-id":598817,"id":"Q598817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178883$FD254FFC-A525-4EFD-987D-1D90E6A625EB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"11ae1b4bd3733396831888ac3494a79d815627f0","datavalue":{"value":{"entity-type":"item","numeric-id":5178867,"id":"Q5178867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178883$41EC2532-BC1A-40E7-BE91-155DE553CE57","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19d34c79dcb21ff5f6ae9d83e7c1b224cf605fc5","datavalue":{"value":{"time":"+2015-03-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":"Q5178883$B27FB438-BC53-442F-91D2-F0DC4C06DBEA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$9EF8D2FE-BD35-4CFE-8D15-86B1C3475381","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$50DA8021-ADEB-4DFE-9D92-6442D6B573DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$5E6C9222-C221-4CE4-8DAA-2879A1A40076","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"809c7f050f206de7c99a5ed24146d8535912a8e9","datavalue":{"value":"6416242","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$A2C86E8C-93BE-404B-9B0E-BB0A158EF045","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":"Q5178883$73CE279A-27A6-4B0E-A34D-9CF8BA8A2B50","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"77ffeb442ca11ab4ee3ccabc804b58b38323bceb","datavalue":{"value":"https://doi.org/10.1145/360204.360220","type":"string"},"datatype":"url"},"type":"statement","id":"Q5178883$E9FD4506-A463-4383-8FB3-3BF888B1FA25","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c4d2a79276bc3ef0b574d726c07943bf9bd147ea","datavalue":{"value":"W1992431017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178883$70794C22-6812-4BD2-B35E-26A129045766","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42240229bec08b4214ce8d197f31f89ee84b3455","datavalue":{"value":{"entity-type":"item","numeric-id":2882984,"id":"Q2882984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0515eaf486ad36574539b7dafb79dfac762c223","datavalue":{"value":{"amount":"+0.7229666709899902","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":"Q5178883$E1D1D2BC-6735-465B-A55E-E0ACF8F2A7C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e54de70359c17c91d77e16505b0af0925517b0","datavalue":{"value":{"entity-type":"item","numeric-id":5387904,"id":"Q5387904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"05d12fc5caaf6cc2cddee9edbd6967ca2560301a","datavalue":{"value":{"amount":"+0.718468427658081","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":"Q5178883$EDD7C45C-9458-467F-BFAE-101C1F3653F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79daacd80091bde89a54cb32e28332e739a62c10","datavalue":{"value":{"entity-type":"item","numeric-id":465685,"id":"Q465685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b884110d59cb951bc85386814eff27fb74988b0","datavalue":{"value":{"amount":"+0.7172433733940125","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":"Q5178883$617DC848-3B2F-4321-B74D-BCC57350F084","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1991339c595d4dc97bb89adbbc394122047a0c35","datavalue":{"value":{"entity-type":"item","numeric-id":2864396,"id":"Q2864396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3046ec0a765670a0655b47d52332edec48a7b7d","datavalue":{"value":{"amount":"+0.7065297365188599","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":"Q5178883$17D3875B-CC39-4536-B35C-C8884A0B1148","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"614e6dccce5295e547dfbcef543b07308b46b90a","datavalue":{"value":{"entity-type":"item","numeric-id":5505421,"id":"Q5505421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a7a53408b060b92bd1e5ce24fd71bb5a5e34ebc","datavalue":{"value":{"amount":"+0.6970167756080627","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":"Q5178883$C1111E25-87A0-4B4D-878B-3621FD2D3624","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5178883","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5178883"}}}}}