{"entities":{"Q3608890":{"pageid":5638796,"ns":120,"title":"Item:Q3608890","lastrevid":50592392,"modified":"2026-01-14T12:19:27Z","type":"item","id":"Q3608890","labels":{"en":{"language":"en","value":"Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5523889"}},"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":"Q3608890$6D2EBB29-FD6D-400E-AD37-6457564DFBD1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1fec1758618bf6ed46c01e8b65c218a5d184a2ad","datavalue":{"value":{"text":"Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3608890$011E3FCB-0B41-41C0-B5FC-09D0761FDD61","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ee5b07ffc602d632511e887047aafa848f052908","datavalue":{"value":"1213.68380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608890$F2F4D004-7934-4A9E-948F-7ACE01FA4C70","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9adba8a1fe1815bd00c82ce2afc885d1c614ea83","datavalue":{"value":"10.1007/978-3-540-73210-5_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608890$863F3C2B-E5E7-406B-B8C1-4B766FCA265C","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":"Q3608890$9338F6F5-8349-4695-AB0F-65AE0A0DC313","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":"Q3608890$8237A8C9-A76E-4D87-ABDB-7733C38E0216","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608890$84D2A35A-47D8-43EE-8C0F-C6EABD83A6B7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19a1026dd4f6172034494e7235e1c6afaf15c529","datavalue":{"value":{"time":"+2009-03-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3608890$86ECBFFE-5B82-48CA-8524-DF7DA32CEECF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608890$E3925BED-D934-40E8-B41C-AA2DC9030BBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608890$FBA6BF7E-C6A3-4CA1-82F9-784FFC8A78CA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e3ec9ae147a742c023f57482603d9f456b353cc7","datavalue":{"value":"5523889","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608890$7E82FB1F-8B6F-4A47-A212-CB4C65F03739","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608890$E30B1065-771E-4B49-A637-EBC13A53BD83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"053189412bee31ec4259231ca609a635f57e0014","datavalue":{"value":"higher-order-logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608890$00EFD038-CFA9-444B-994C-2673EE16DF99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a43c47dec4220d9a6b5b780b7cd50a4fe76e3881","datavalue":{"value":"probabilistic systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608890$3C814A84-E4FE-4AF7-8CAE-98BD4ADE0D9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62da53b47174b048d375db5f0faf9f4469ffca9","datavalue":{"value":"cumulative distribution function","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608890$111C610F-1037-42D7-8361-95D10C00CCC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5343ecd15a8e87cb138c7d9e4c8f0d52a5afdb65","datavalue":{"value":"HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q3608890$15A0DC70-466E-4FB6-887B-B50134B49BC0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85abfddd32bad4b2678f5ebdaaec764a410b76c8","datavalue":{"value":{"entity-type":"item","numeric-id":20941,"id":"Q20941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3608890$98258F6C-80E1-4FF3-BEB6-71DA40FDE8BA","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":"Q3608890$4B9FAF05-0B85-4A8D-8550-DED70BD6E330","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9db9ac0b5a26a117380b3688478dc89c1fb2c34e","datavalue":{"value":"https://doi.org/10.1007/978-3-540-73210-5_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q3608890$339A7FF1-0DC2-4902-BEA5-AB1C306E6DF3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0de7c182aabd600b87b461473c097970f8219a61","datavalue":{"value":"W1595825122","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3608890$D8E9B299-9678-44C1-AA0C-0D407E0D7504","rank":"normal"}],"P1643":[{"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":"5b037dd070c15c0b025db05baf0f0e879b69366e","datavalue":{"value":{"amount":"+0.7837299108505249","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":"Q3608890$2163D7BF-B36F-4362-8B9E-93C2F0472470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d518978192920843b4db21a03d57b8d0b217ba3","datavalue":{"value":{"entity-type":"item","numeric-id":3608329,"id":"Q3608329"},"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":"Q3608890$C8AE165F-0B55-470B-AAE5-C6BEB4503879","rank":"normal"},{"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":"abfc97d053b90859d2b3f1262788a5d41191a9e9","datavalue":{"value":{"amount":"+0.7540695667266846","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":"Q3608890$F54BC929-9D1C-41A1-86A3-E58E984D09E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ff311b2b3ddcf8a75942e9b4d3c781c58e520dd","datavalue":{"value":{"entity-type":"item","numeric-id":995466,"id":"Q995466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6f93c21a09dd68f80df7993ebbef570f6d6cc26","datavalue":{"value":{"amount":"+0.7473406791687012","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":"Q3608890$FE8B4657-4FEE-4CD1-863D-712F1E6A28E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f9b5625db721d32945bb558344f44be3d4db9493","datavalue":{"value":{"entity-type":"item","numeric-id":545151,"id":"Q545151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"febc769468dd20b22178fee4f843bab66346c63f","datavalue":{"value":{"amount":"+0.7407644391059875","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":"Q3608890$14A22320-EC0F-4AB9-B8C1-CD1B944E54DF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3608890","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3608890"}}}}}