{"entities":{"Q3608329":{"pageid":5638235,"ns":120,"title":"Item:Q3608329","lastrevid":50590436,"modified":"2026-01-14T12:11:26Z","type":"item","id":"Q3608329","labels":{"en":{"language":"en","value":"Formal verification of tail distribution bounds in the HOL theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5523083"}},"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":"Q3608329$B2D17E68-69C6-4D83-809D-6E3E95CEAF4F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dac206b8c4e1a4f2fc290a304de82391cc2f8357","datavalue":{"value":{"text":"Formal verification of tail distribution bounds in the HOL theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3608329$A1EA6656-601A-4311-91C4-86595BBC3480","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2f4e4c9f16392ef294c2e6644984a617655e9403","datavalue":{"value":"1167.68053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$5835F3FB-0D2D-4B0B-B0BD-5B1E3A4338E0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"393ef07e7673f4510d0e5689d2d44001b3ecc236","datavalue":{"value":{"entity-type":"item","numeric-id":246140,"id":"Q246140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$E2E7EA09-471A-4297-A0A6-B8A2F6960FC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0d2c11253a443ddc53e205509995096ef6b865e","datavalue":{"value":{"entity-type":"item","numeric-id":246141,"id":"Q246141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$1EC789FA-D100-4B3F-9158-C4E7BAEA581B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a9b4f623f6152b37a1167395eeb5a29fb9ff8f6c","datavalue":{"value":{"entity-type":"item","numeric-id":2714900,"id":"Q2714900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$8D03A6DF-98E1-47DF-B69A-BBA7CBC3138A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3434863a4c3842a9ef45eb54b7cfeda15cdee482","datavalue":{"value":{"time":"+2009-03-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3608329$5540695F-CFD8-42B2-AF44-C87A29FFE8F3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c9ef8c5be016f0ccebe5d051335def1e699f75c1","datavalue":{"value":"https://spectrum.library.concordia.ca/974500/1/formal_verification_of_tail_distribution.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q3608329$A1080723-C319-4CA3-8D7B-2C36D6828B02","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$FA571508-BF5D-4F83-8E0E-A70D743FE0A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"573684ced2fe2c188247678e777849505e146cb1","datavalue":{"value":"60A05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$4A2EB2DA-CB30-4FFB-96D1-1224A3DCD236","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fedc54d041dbaf3922f156ba09e5514c44ab5169","datavalue":{"value":"60E15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$90F7154E-F753-449C-9DEA-CF4F72F9A487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7ddaa80bf0a693a36c1113ff6b7ad576f729940","datavalue":{"value":"68W40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$9CD7DEC7-D37A-41E0-9279-8C8BEFE8FAC5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"912a66146e9367b558b8a9a555fc1a4c40ed18b2","datavalue":{"value":"5523083","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$102A5DAE-478C-446B-B4FA-86DE02EB3A8B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"19da48970ad57aca055230c5985123cd5e6e689f","datavalue":{"value":"Markov inequality","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$2B5A8330-9B66-4699-8766-AC141B674975","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8fb9293de76ea341aac800812f0f833a82a630fc","datavalue":{"value":"Chebyshev inequality","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$230F932B-F6B0-4358-844D-08D5EB641528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d2dd32f2dd42c05a6b527dca9a63bc990b396e6","datavalue":{"value":"discrete random variable","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$4398D70A-869C-4AD7-B59C-33785C0FC2F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82a73e764b019f700c8d12fef8a1e8779a2463b2","datavalue":{"value":"mean","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$AD4E7152-CC1F-45B9-9CFC-117CEFEEB429","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d04ce3d9f3561d73173b1852bd83082b782ad6eb","datavalue":{"value":"variance","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$BE48C004-DDD9-4B3F-808B-A9A031C4BB21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$9F26F9F9-177E-406F-A964-336EECDB1169","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"508c4d325a0409b1410c8a3854c6e11a7edb3a8d","datavalue":{"value":"mechanization of proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$2E7FCD71-4E7C-4823-892A-FFC95338568D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3b6a700a002c6fe1fcd568fbdac44e45ecfeda53","datavalue":{"value":"probabilistic analysis of algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$C727A3C9-7F67-453A-83E1-78E538805CFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608329$0B5F17E2-136D-4943-BDC4-044439B3A634","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4d9e3398f9a03c25d17ec7e1e092f704c058607e","datavalue":{"value":{"entity-type":"item","numeric-id":20434,"id":"Q20434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$C6C0A37F-6553-4909-B924-C51D48D3BC5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$CDD22F4A-7097-4389-B544-D3C747F16B47","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":"Q3608329$1E9FB787-BA3E-4346-AF32-0E826750370D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"27d1979df93c4f737cb44e15f9d208a926cc101c","datavalue":{"value":"W2006220703","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$D005605B-6EB5-48BE-8406-E8314E588DF4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"82ba3bd74ef41e0757015be3b53bca7ad9cb71ba","datavalue":{"value":{"entity-type":"item","numeric-id":5463630,"id":"Q5463630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$33FB3CF0-E017-4CD4-B814-0CEEE2EDD287","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a59763b3fb25129051745803dae70f5cf79103f8","datavalue":{"value":{"entity-type":"item","numeric-id":4484343,"id":"Q4484343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$87AFD556-8F1C-4A56-9B23-B0303EBCFA0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d84002c228353cd557a130622cd1ec8dc59490cb","datavalue":{"value":{"entity-type":"item","numeric-id":3523170,"id":"Q3523170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$BD5E6023-23A4-417D-BDF9-DB16DECD151C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a56ff31e12d13be9abbbec8c780fc7a1ba4c67d3","datavalue":{"value":{"entity-type":"item","numeric-id":4712216,"id":"Q4712216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$FC0E401D-E9DA-4089-8E91-C1E399F6442A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bc22eda20e13ae4c1f389d048db76ed6af41ab3","datavalue":{"value":{"entity-type":"item","numeric-id":2849848,"id":"Q2849848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$DE857F82-5BFE-490F-907D-910A070C04DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$079CDC43-9C03-435F-B4F9-CD9FB165E853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"436d4ddccf9258c9f31fa193f202f774ffec18b8","datavalue":{"value":{"entity-type":"item","numeric-id":1250704,"id":"Q1250704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$26AABCD0-E5FF-4284-9B53-883705790645","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$3DAD438E-AAB2-45D1-94A4-96031891F013","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$19AE5674-FB46-4558-8725-3FA1B687F3A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc18b84f53cfdc559b4d296e04ba30186fce5df8","datavalue":{"value":{"entity-type":"item","numeric-id":5464655,"id":"Q5464655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608329$B01B3869-CAF8-4D9E-B072-BC1CD5E83217","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0d8658be24a28510018c8a094a523b58c1b4a6c4","datavalue":{"value":"10.1002/MMA.1055","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608329$16F8784E-4CD9-44CA-A80F-C094BD31CA6B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"82ebad7efbc5727c6ace3042f64fccced6d2b2ee","datavalue":{"value":{"entity-type":"item","numeric-id":1040780,"id":"Q1040780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6bb84407f2d7b7272161fc0ee8cbde79ce1b6c1","datavalue":{"value":{"amount":"+0.7865179181098938","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":"Q3608329$0A27B8A4-B246-499D-8BF2-F365D7DA66E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"58eccacf9a1cb87a6affdef33b66ab54671b4488","datavalue":{"value":{"entity-type":"item","numeric-id":3523170,"id":"Q3523170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb68f57365e522cfc5ade4226306fc580023663a","datavalue":{"value":{"amount":"+0.7650284171104431","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":"Q3608329$4FE792B7-CBF3-4423-B5F2-B8D072D0D550","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a29a6aabaed4c931eebeffef7ee595826d2a8eb","datavalue":{"value":{"entity-type":"item","numeric-id":3608890,"id":"Q3608890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8192e85999b32ce64af4d396485eddfea76330ef","datavalue":{"value":{"amount":"+0.7605413198471069","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":"Q3608329$BC7010D2-2A3E-456A-8DB7-31E3EB6C4293","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a19e6f174761724f8839f43fc4c60871a2678df","datavalue":{"value":{"entity-type":"item","numeric-id":2434565,"id":"Q2434565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44de9eb9ca208bae688018a726c06e9231eeaccb","datavalue":{"value":{"amount":"+0.7126018404960632","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":"Q3608329$DB6E2FF0-BAE4-461E-8E95-44B437AA3404","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43f7e500bbfc468599a5544958ae233332d636dc","datavalue":{"value":{"entity-type":"item","numeric-id":1791202,"id":"Q1791202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eeee06450094f8797c616a1a30f9f11e24c1f6f8","datavalue":{"value":{"amount":"+0.7116333246231079","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":"Q3608329$7772F569-BB7B-4BC7-8EF7-66774F995EE5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3608329","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3608329"}}}}}