{"entities":{"Q1701041":{"pageid":1711782,"ns":120,"title":"Item:Q1701041","lastrevid":68169765,"modified":"2026-04-12T21:53:56Z","type":"item","id":"Q1701041","labels":{"en":{"language":"en","value":"Markov chains and Markov decision processes in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6842149"}},"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":"Q1701041$8A93C2E3-A0BF-440D-9AF6-1F239D6738CF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fbb07d3973846619b5ce3b33755f85b33c914957","datavalue":{"value":{"text":"Markov chains and Markov decision processes in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1701041$6A9F96DB-8E47-4795-A186-B2DCD2CEE0FE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a114c06bec9a1d0f65bf1787b5de985b5bb150d1","datavalue":{"value":"1425.68375","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$B48B2AD3-06B8-42D8-8001-F581480A805C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"26d6620daf8648b9713aa99490f0508510abdae9","datavalue":{"value":{"entity-type":"item","numeric-id":1687531,"id":"Q1687531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$3C5B13B7-B8DE-470B-896F-24A1AF65A3B1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$20F9D861-B518-4FF5-A028-87D14E233EDF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4c98dc438f41659f2d190c3ff2966dca049d17da","datavalue":{"value":{"time":"+2018-02-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1701041$11384E47-BD0C-4FCF-A446-C5578F336DF3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$949DAEFF-8BE2-48FA-8746-653B2182BC69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1cdf15533e26fc0c4c2e22d28e655c364dfe77a6","datavalue":{"value":"60J10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$5E989D40-5A50-4713-8EFA-BEBE4E53F8B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$547F318C-1344-4C62-811E-7CFD52511986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"377d3ab03372cff12915e0de0374438ff70c3716","datavalue":{"value":"90C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$6A6CFFD1-7ED3-4588-AC31-4D4DBA9ECED2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9a9898d6c3d0b80936082ea911e9ea0f43c91286","datavalue":{"value":"6842149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$FD7DDC38-9992-4C87-B7F9-182945807D14","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"54386443767439a4565bd3fedc3d37d2c4a4f85d","datavalue":{"value":"Markov chains","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$AE36E7F6-3BCF-4D6E-A87E-DBA2CEC376FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fbd1f99995fb6a13da62a377ba6327166316e976","datavalue":{"value":"Markov decision processes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$51596EF8-AAA6-4E11-9598-008D60E5CEDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"185237d9a3d532807ca9d21a85579f9cbb068959","datavalue":{"value":"probabilistic guarded command language","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$F96085BE-7AED-4F77-A16B-C97CE338FEA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14fdb321d63e54de1f24ee42307b3934b281d990","datavalue":{"value":"probabilistic model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$822A7CBE-6E7C-4FBA-92F8-C0E347D9E40F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fbfdeabc9d9c8d23822e01288875f022a98a7da0","datavalue":{"value":"coalgebras","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$C3467226-3A2C-41FC-A6AA-8E55B6998FF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d9c2e1f00facc619242af9af43a4aae006f38ad","datavalue":{"value":"transition systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$FF7808A7-52FF-4ED1-AD2A-F382CB218825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3c5932807119e47a44498f546b5072b5739a4ec","datavalue":{"value":"trace spaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$E5B5A6CE-FCB3-4DE8-935C-2C48C3FEF07B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1701041$B4CF4BA3-0D16-45D4-95AD-AB9395917DCC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ae4173d13b960594f2bf5bfd22402fc0202f2b76","datavalue":{"value":{"entity-type":"item","numeric-id":40255,"id":"Q40255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$B98B76FB-6CB7-4004-A131-5FAFC722E4D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$F987B7B1-C213-46BC-A8F7-5AB8686A7D61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b1d7c89f8c4a43a132064ef87f7add4215ef6c5f","datavalue":{"value":{"entity-type":"item","numeric-id":16314,"id":"Q16314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$79A55AA5-59FD-4AE7-A46D-218785B493E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"531a52a4ab12ab6e2b5be84834036762ed677445","datavalue":{"value":{"entity-type":"item","numeric-id":13928,"id":"Q13928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$EF1EB7CB-A5D6-4130-B889-5FE437399082","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":"Q1701041$0E748D98-1C54-4537-ADD9-0AC605B82A4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e9fd7dbff509abaee9c64d21afb19f85055bad01","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$A7453FAC-9773-4746-B46C-C1A032B74061","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1f427ab6dbbd025b0c0b66dd047be36c332e9e80","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$043222F0-8D1D-4097-961D-FF7E4C94DEC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d9f40cc84fcbe9941b7cde39aab30182ad6ca74f","datavalue":{"value":{"entity-type":"item","numeric-id":40246,"id":"Q40246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$D43BB748-0F5B-40FA-95E1-C0476A81764F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f6907c99f108b6e9bb16dac439b2e60825fd3f4","datavalue":{"value":{"entity-type":"item","numeric-id":40290,"id":"Q40290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$E255B7C0-4BD0-4064-A074-079B0D2819B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"12939772fc363709f781c5699946bf5e9d5e63eb","datavalue":{"value":{"entity-type":"item","numeric-id":40373,"id":"Q40373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$1535F158-5212-4EFC-BA9E-C592FEDB46C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0fac9fb5cfad6545c88cc8857964533dffc3ed17","datavalue":{"value":{"entity-type":"item","numeric-id":40544,"id":"Q40544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$01B37FCA-95B2-4C51-9488-FCECA4C76AC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$5910D44E-22E2-4015-934E-E4A6843887E6","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":"Q1701041$32306135-C7DF-45F3-A78C-F6C31BCE394F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"195b539a733384ed66d94ae33075eab4517be420","datavalue":{"value":"https://doi.org/10.1007/s10817-016-9401-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q1701041$3D5A5E9C-B270-4AC2-88A7-A7029E289DC9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6b5b2a9660ac00901e3fbf36fbb35a6c076af3e8","datavalue":{"value":"W2562825158","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$249CA3AE-E0DC-41D5-B21B-FA03B033C528","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb21a49f130376afad51708fa20a730cc6a313b9","datavalue":{"value":{"entity-type":"item","numeric-id":2352494,"id":"Q2352494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$EDF26AFB-D999-4EC5-AB58-1B81D952BB0E","rank":"normal"},{"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":"Q1701041$D31903F9-9B9B-454F-B084-10D9107B43AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30934abbc32128e5c1a91e04943aee41658d6f31","datavalue":{"value":{"entity-type":"item","numeric-id":1694568,"id":"Q1694568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$988904EE-A2EC-4231-B8EE-1A4557DF89A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28b8f2843a7242ba011aa6e7f33280202a937137","datavalue":{"value":{"entity-type":"item","numeric-id":4738112,"id":"Q4738112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$BA6DB58F-A27E-4741-8F78-23C2F0E0FAB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b0c7436976c5b9893e05c1462fed16a80d7904d","datavalue":{"value":{"entity-type":"item","numeric-id":5322945,"id":"Q5322945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$829A7F41-07AF-421B-8679-4A3787D30ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7618dba3c858d60e577e7b915b9ef7225ee18f34","datavalue":{"value":{"entity-type":"item","numeric-id":3452195,"id":"Q3452195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$CAC8678D-3354-4429-A7EB-EA8B679A2ABB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d993f7be3ea77cad4a800be898a39b5ce70ed5","datavalue":{"value":{"entity-type":"item","numeric-id":2879246,"id":"Q2879246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$F8E0B1C1-B877-42DF-88E7-679CEEC5E621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0202cb9cafa0358b07911808cfce41ae5240485b","datavalue":{"value":{"entity-type":"item","numeric-id":3192180,"id":"Q3192180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$1DFED95E-A895-4CDD-AAFA-0858CF6B014B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf446b5419b8e3a70a44aff75bbc12fa8bd693c8","datavalue":{"value":{"entity-type":"item","numeric-id":2391534,"id":"Q2391534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$10A09DB4-CE9F-4170-9C60-A95B1A045383","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7912fa5a59a9d011428d7449cacc55f320ac1a0b","datavalue":{"value":{"entity-type":"item","numeric-id":4658722,"id":"Q4658722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$6D0527D6-4C63-40F2-8D85-C6B4454BB1CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f278fb8f0b94aafeed03fab9bd29e989c7db3162","datavalue":{"value":{"entity-type":"item","numeric-id":2568451,"id":"Q2568451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$F3057CFD-B44A-4B4C-BD0F-AC6C4285CBFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ba4f5628b9493b3dc4e9b69bc068cb07ae68c2f","datavalue":{"value":{"entity-type":"item","numeric-id":4530231,"id":"Q4530231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$2BAEEDB8-1BA9-422E-8FAE-E42D34FA28D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17d3bf53e94a938d4f9a9fcdc3603c5ab6b47000","datavalue":{"value":{"entity-type":"item","numeric-id":5709980,"id":"Q5709980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$9C787DC3-39F3-4CB5-AFFA-95C72CDF2AE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f5c5f6db121a6cfd9285a3ab5f1d994402b6524d","datavalue":{"value":{"entity-type":"item","numeric-id":2802431,"id":"Q2802431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$0C37A164-AF9B-4A99-8BDC-7974F34D3DD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a9d1825e985bd9d3ac22966e44befbddbae3977","datavalue":{"value":{"entity-type":"item","numeric-id":5310649,"id":"Q5310649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$4043CE06-F1BF-4813-8EFD-17978BFCDCAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cdef39b443c7c711b01a47d68a2506772be4e26e","datavalue":{"value":{"entity-type":"item","numeric-id":3946875,"id":"Q3946875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$408B643B-3AD4-4FA1-B134-1B7F92A5A34D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16b4b9eb7104682bb03b01e94a3a4f2c998deb92","datavalue":{"value":{"entity-type":"item","numeric-id":385988,"id":"Q385988"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$E348B69F-C9A7-4DF7-9AE5-4B0F0481B4E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af3e2377138664b02f380d31d39eb16bce1045df","datavalue":{"value":{"entity-type":"item","numeric-id":5364260,"id":"Q5364260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$6A254B13-5E2B-49C9-AC1C-47CBA1B7EDB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78c7d2585bbc0e61d6a06515c003be877f00a2b2","datavalue":{"value":{"entity-type":"item","numeric-id":3447700,"id":"Q3447700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$14F15608-74F8-47A7-BC57-9703E52A4C7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e53d9e53c3c574e8c7675f6ec5036e8ca0ad199b","datavalue":{"value":{"entity-type":"item","numeric-id":1343864,"id":"Q1343864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$867C618A-5285-4901-939C-05FA043A812B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3710c9b6ddf8dbb24e135f3387ab935865a76ef6","datavalue":{"value":{"entity-type":"item","numeric-id":2829281,"id":"Q2829281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$16974FAA-39F3-4FFC-90F0-0E80376A9DB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34dd873a66486e9e38fc156a4b8aa6ba19960bb7","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$C9993B05-9424-4D48-8C46-3B6D6C50793C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d360f4c10b4163627f57faa3db163275ea6a011","datavalue":{"value":{"entity-type":"item","numeric-id":5327350,"id":"Q5327350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$3E97D574-312C-4ADA-B28E-478F70C3552D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8bfb4cfac567a097f2a651df3bdc8285a6e2cdc","datavalue":{"value":{"entity-type":"item","numeric-id":2945633,"id":"Q2945633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$A7FECFA5-5BC4-489A-891E-69E8694DF9B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b29ad255f0f1fc43ea69d59d95eb9a24cc08b4d4","datavalue":{"value":{"entity-type":"item","numeric-id":2894281,"id":"Q2894281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$AF6CB752-31F0-4A87-946E-8F6CFF60C56E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$69A22500-042B-4550-9C7C-BA5DD424B77F","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":"Q1701041$AD8FEEBB-367C-4DC2-8599-5D0F24E84FC7","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":"Q1701041$3556A1FC-68CE-4DBE-9223-A0D6CDDEEEC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"753bfe30e08a7e82b0acc716c863fd1bf7ed17e1","datavalue":{"value":{"entity-type":"item","numeric-id":3084591,"id":"Q3084591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$57D18013-5CF6-48D5-899C-20D3A93B45F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93505c77dab5a1e19c66339180d2a22efb3304a5","datavalue":{"value":{"entity-type":"item","numeric-id":5327351,"id":"Q5327351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$DACE31BB-61DC-40DC-A8CB-C7B3992E3954","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a334f4e96bc67eac9a5d7b987fa6f5d79a92b99","datavalue":{"value":{"entity-type":"item","numeric-id":2802495,"id":"Q2802495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$67162DAF-E52A-4673-B7C0-F8D40F7469E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c1591307efdcfd25c5361ed6b6bc0d30639a1f8","datavalue":{"value":{"entity-type":"item","numeric-id":4650346,"id":"Q4650346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$AE6F1113-B8D9-49D8-B935-953954DC8691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98f646342823069d9bf888488cf5680b13ceeb69","datavalue":{"value":{"entity-type":"item","numeric-id":2781467,"id":"Q2781467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$533DFA5C-D2DC-4855-B096-89BCF0AAA19D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e210f1c7125a47cdccffe2dd09f5c241337587a","datavalue":{"value":{"entity-type":"item","numeric-id":2938053,"id":"Q2938053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$AE2E910F-9751-4280-86B6-43A5BD32BEB7","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":"Q1701041$306F71A8-70D4-4852-9E06-F103F2C356CA","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":"Q1701041$1D3092E5-16E8-42BE-B06B-9AD6FCAF57F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cfc6615329733626bce9f1815a0b2348420e0db1","datavalue":{"value":{"entity-type":"item","numeric-id":3658792,"id":"Q3658792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$2AE06CD0-6334-42CA-80FC-23E508B06B81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b898799284c8526436844deb549a7de9b888620a","datavalue":{"value":{"entity-type":"item","numeric-id":834045,"id":"Q834045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1701041$357B6771-4B75-484E-8E07-6C1835BB09B9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a330adbd2dfc77a0a25eb8a527091f9a592cd4e3","datavalue":{"value":"10.1007/S10817-016-9401-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1701041$416F3FAD-3316-4EA8-A7E7-E3B0CBDF18B9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36771dc220ddf60909b37230830c74f27aa673cb","datavalue":{"value":{"entity-type":"item","numeric-id":3172906,"id":"Q3172906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2a3819b708d8193b4e84a267911b4b99c1367532","datavalue":{"value":{"amount":"+0.8158484697341919","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":"Q1701041$7319F380-63B1-404F-831D-8EBCB2705CB2","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":"cfa0e14482a558c7c73bd24c10b97b3f39c073bf","datavalue":{"value":{"amount":"+0.7858045697212219","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":"Q1701041$489301F0-AC67-442D-A874-4A06F45902DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5506e27296ee335d165e07718f33f18f1ef09e4f","datavalue":{"value":{"entity-type":"item","numeric-id":2945633,"id":"Q2945633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"988dcdbc411d1b77d312ea0e75c2851bed89bfe4","datavalue":{"value":{"amount":"+0.759504497051239","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":"Q1701041$7A56AC57-1E92-415C-A05F-76E80711A583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f1ca6a44dff35ae963ab52828ab4a54c23b8bc9","datavalue":{"value":{"entity-type":"item","numeric-id":3090817,"id":"Q3090817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db4243c2bf1e2ebebe69b195db4af9e18a461eb6","datavalue":{"value":{"amount":"+0.7491304278373718","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":"Q1701041$5F5761A7-5C28-48BB-B524-F29C98D1EC1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"312b4c6001ad00eb7f145f069abe7b68afcac201","datavalue":{"value":{"entity-type":"item","numeric-id":5327351,"id":"Q5327351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f325b45bd171d2bae86da31df8d6439a05f6b24","datavalue":{"value":{"amount":"+0.7468083500862122","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":"Q1701041$3A65C36D-BE71-4DFF-864C-99EB9EA227FE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Markov chains and Markov decision processes in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Markov_chains_and_Markov_decision_processes_in_Isabelle/HOL"}}}}}