{"entities":{"Q5971408":{"pageid":8148204,"ns":120,"title":"Item:Q5971408","lastrevid":97794392,"modified":"2026-06-05T15:25:45Z","type":"item","id":"Q5971408","labels":{"en":{"language":"en","value":"VPHL: a verified partial-correctness logic for probabilistic programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6664941"}},"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":"Q5971408$CD113D3C-7DAC-44DB-AFD0-DB664D6FA60D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dae6b0a00afa6809c4306b6e6903e86758ae4206","datavalue":{"value":{"text":"VPHL: a verified partial-correctness logic for probabilistic programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5971408$1B49ADBB-9F1C-4FF0-BE9E-8DD7275CD819","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1f84a233dd1cf8b9b6743775ed5a3960c2b74a43","datavalue":{"value":"1351.68080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$24088481-E860-4376-AB23-5F8917C230D8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$1E405DBE-7E77-4177-AAFE-7839A2710AEA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"81dc7daf8e9d74fc43b1651d3815e34e62e970ab","datavalue":{"value":{"time":"+2016-12-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5971408$D620DFCD-5E61-43EE-BEC2-7710E6DFC371","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$7529BB20-38FF-4E85-80D4-14B65259FEF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$207AF7AA-BCCA-4CC7-98F4-CD83D2760132","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35c3f01235ccba091e1644bb05c86f53d45fd7f7","datavalue":{"value":"68N19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$24CB210B-15C4-45BE-9DA7-60204F7A62F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0dd26fa594336927a7a04e8147a405d69e5da239","datavalue":{"value":"68Q87","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$35AB74C9-D781-4435-8C0D-583EF9ABBA81","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"57c203b84ba7e5a63ae4d469093764a9eed2dede","datavalue":{"value":"6664941","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$398B8C88-0FEF-4E37-B449-B88D9D0C3B4A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5971408$CCBC5E18-2459-416F-8FA2-BF7AA592181B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5971408$5648C8FD-D1D7-4D0D-942C-858B2ABD7C2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5971408$A79C947F-9FC7-4943-B849-3181725D0DFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2bf78c9ff68381ba2adb2a75ba12d4f7a7246f85","datavalue":{"value":"probabilistic programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q5971408$C1249ADF-8CD5-4AF1-9342-4BA1D7E34507","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54efe8b49a37b1aa489fb0e653d938725cf2fcaa","datavalue":{"value":"non-termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5971408$47E9F57D-7BFC-4116-A7EA-076F8D5972D9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$F1A3CAA8-FA6C-405F-8288-11B08D1093BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7fe59170fba346830227c00c080c8ce49c25355b","datavalue":{"value":{"entity-type":"item","numeric-id":44932,"id":"Q44932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$BBFE46B2-D00F-440D-AF03-F08668A85CFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7b8bfcbbb8584ed9cd8fa8ae699d0634f4084a68","datavalue":{"value":{"entity-type":"item","numeric-id":21717,"id":"Q21717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$EBAB6DEF-7C4F-4BC6-852E-198494A1E95F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c35911ee98ff2de6334d1e2e50eda7a0f208d4c2","datavalue":{"value":{"entity-type":"item","numeric-id":24997,"id":"Q24997"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$D117E17E-33B1-4AEA-8ABE-FD93C275804A","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":"Q5971408$620D7C6B-A888-450C-A7B6-0CE685CB081F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"03c488349499052c7a56efc1aede134c5f8a1978","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2015.12.021","type":"string"},"datatype":"url"},"type":"statement","id":"Q5971408$EF774DE9-E4C8-4B96-8E51-A1F9964D08DB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0443268cc30d0c1136f8e93c86fb3e8be967f41e","datavalue":{"value":"W2220918360","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$DE575E16-4469-40A9-9218-301AC1F25537","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"144a308c592ec4ad42a7f9f35546e3a8be13a1a4","datavalue":{"value":"Q113317720","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$0211D34C-3498-4563-A0A3-ACAA8A30151E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1370d4ef41cfc490a43b42eec581952d43ac681","datavalue":{"value":{"entity-type":"item","numeric-id":923886,"id":"Q923886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$70149D28-C7FE-4CA8-8E82-5EF08CC45351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d16eb2457f1ae3593ef05e516dcd31f598ca1d8","datavalue":{"value":{"entity-type":"item","numeric-id":5253588,"id":"Q5253588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$0D0B92A2-07A1-4744-A130-9C35D657F5BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd4c931786d4fc7c311f2d1f8f393efad02baa34","datavalue":{"value":{"entity-type":"item","numeric-id":5199185,"id":"Q5199185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$F49BCDC3-46B6-4D77-919B-DAF837AEC7CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba5ad8860e2dfafdd492a4ade42b23f462631c32","datavalue":{"value":{"entity-type":"item","numeric-id":5261508,"id":"Q5261508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$60874D5E-B3B7-4189-93A1-59987E14A728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"902d58911cf57d61e4e30d431d92c375a51f10b6","datavalue":{"value":{"entity-type":"item","numeric-id":3452246,"id":"Q3452246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$C9F0B4A3-85FF-4213-B7C6-3FB16EB6FA6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"797020f33bcb505e6b7d4ea91449a8c0b95864c3","datavalue":{"value":{"entity-type":"item","numeric-id":2373709,"id":"Q2373709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$E31DD512-AAF1-4510-981A-E8D6378C641E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc2df5503548a1f952fefa1e0d56e4ea0eb75c55","datavalue":{"value":{"entity-type":"item","numeric-id":3613341,"id":"Q3613341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$C5F21282-724A-43DF-8C36-88F252AF170B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2596fff7a43cf9dae167e4a3260a86eb026f5650","datavalue":{"value":{"entity-type":"item","numeric-id":3021957,"id":"Q3021957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$BC640CBA-1183-4B08-8238-75DBE9BC3866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$D6300B83-1259-404C-A714-DEA456B0F7FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f81309e87becee3cda8d7174d2d8b5b31baaaeac","datavalue":{"value":{"entity-type":"item","numeric-id":2576950,"id":"Q2576950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$1ACF5A99-5D3F-4BB2-9940-68DF23188777","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3832e3dc267ceb2e4bb4d3a758f9c5723b89426b","datavalue":{"value":{"entity-type":"item","numeric-id":1159979,"id":"Q1159979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$F167FC29-389D-4019-AB33-DEEEE1BE48A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f182afa47ea37b09a1d1a3075ffe1edef8370b5","datavalue":{"value":{"entity-type":"item","numeric-id":1063584,"id":"Q1063584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$A94A5A20-8CA2-43CA-83D1-6CFD41360FCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14f29bbeded03b5c34676a0e50a74637f09aaf8a","datavalue":{"value":{"entity-type":"item","numeric-id":5459189,"id":"Q5459189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$EEE93B28-FC22-4EA2-BD38-7F705A5AA673","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f01e77b2c8dc769c5ab3929411452edbf96a4b","datavalue":{"value":{"entity-type":"item","numeric-id":5971408,"id":"Q5971408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5971408$D6E66538-DA09-4012-B1D7-97599BB76105","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"541a9f9391e8f606b8657d9ca362bd2fd9dd011b","datavalue":{"value":"10.1016/J.ENTCS.2015.12.021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5971408$19FFC5CA-B4BE-4B9C-A5B0-AF69B21D7756","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"069e430bb430cd217bb003a396d40fed1851271a","datavalue":{"value":{"entity-type":"item","numeric-id":3021957,"id":"Q3021957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a425982b44ee00c813aed38bfbbbe5563c74abfb","datavalue":{"value":{"amount":"+0.8373278975486755","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":"Q5971408$8247112D-8FE8-4C17-AE4C-445D86C3CD80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb78fb0ce6e11fbb4974fcf12abf053d1faa2f28","datavalue":{"value":{"entity-type":"item","numeric-id":4501575,"id":"Q4501575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"192d73e4421839d4225ab4af6306036337e3461a","datavalue":{"value":{"amount":"+0.8339883685112","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":"Q5971408$40B0F533-5EBA-49C7-9F38-52475C555D36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9c2f2a7fc8474c0133780afda7d6c98adfa044d","datavalue":{"value":{"entity-type":"item","numeric-id":3316558,"id":"Q3316558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"449fe5bf72a3397fbfcbf22660e6b5dc943e3d2d","datavalue":{"value":{"amount":"+0.7919908165931702","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":"Q5971408$2DEE5991-09AE-44D0-BC78-8C89087CA5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68762eb4d0ade5d59d0e2ff7deb1512c1b85bdb2","datavalue":{"value":{"entity-type":"item","numeric-id":2323970,"id":"Q2323970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0b5f0135571dbe49b88997fa0dde2dd90b8e339","datavalue":{"value":{"amount":"+0.7874939441680908","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":"Q5971408$37DF16F2-8C4F-4AF2-A922-81E6FDC90F92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f13c8d9de74e207d5264761e759f38366e34d09b","datavalue":{"value":{"entity-type":"item","numeric-id":792757,"id":"Q792757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76fa4e9c98464f4e6d56d1cb81d44f25f91bfeba","datavalue":{"value":{"amount":"+0.7670904397964478","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":"Q5971408$67C68D09-ADEF-48E6-AA67-E3BF4EA4B71D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"VPHL: a verified partial-correctness logic for probabilistic programs","badges":[]}}}}}