{"entities":{"Q5410477":{"pageid":7440051,"ns":120,"title":"Item:Q5410477","lastrevid":51979766,"modified":"2026-01-20T16:32:47Z","type":"item","id":"Q5410477","labels":{"en":{"language":"en","value":"Algebras for program correctness in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6286088"}},"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":"Q5410477$5A8C59A0-27B9-4467-9AE5-997DB74EFEA7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a73ca6754ce72c9c22bce97dc2f9c3e4298142b5","datavalue":{"value":{"text":"Algebras for Program Correctness in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5410477$C0C03BE8-1B4B-4FB1-85B9-3D5C2682EF3E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e431a8d32e71f0376bad941c24072a18495f352c","datavalue":{"value":"1405.68314","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$AC7897B7-8A2F-4767-81AB-4155837B2EF4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"628bab6ab67ea77537fdbf101e3e56225cd63c6a","datavalue":{"value":"10.1007/978-3-319-06251-8_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$CF76B733-FF58-4D00-9B80-463F7A0BC2D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"661058c43babba56430a6ee50eb96105dced91de","datavalue":{"value":{"entity-type":"item","numeric-id":406432,"id":"Q406432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5410477$B4BD9636-FCE2-437C-84C3-0E1BEBBE47CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"07e74b055b7dcafad92abeddbcafba2bc598685c","datavalue":{"value":{"entity-type":"item","numeric-id":736460,"id":"Q736460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5410477$8A2EF858-E51F-484A-B1E5-8875F0CF0DB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb27aad50a775f188aa99887f496d209cf025869","datavalue":{"value":{"entity-type":"item","numeric-id":299200,"id":"Q299200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5410477$3DE5447F-50DB-4143-AA44-C974EF3513FF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"40b55b51d1711e94124c260c7ee2d3d6bc2c1162","datavalue":{"value":{"entity-type":"item","numeric-id":2915131,"id":"Q2915131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5410477$77045922-FBBB-4A9E-8A97-CC3074478A37","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a3c251b63516e63161db6918c2e83c80c7676385","datavalue":{"value":{"time":"+2014-04-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":"Q5410477$95956E3A-B821-42BE-9C34-D2AE1531CCA0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$C2CE6DE6-AF75-4CC9-9B55-8D5E4150065B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$24099D32-5A54-40D8-B922-AE95A570C7D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$7D1B2719-E653-41DB-97B3-57B289DD87CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"deb5f9f43f355c6575c467b17adc4a680e013b41","datavalue":{"value":"68Q70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$BF3D3640-F772-41C3-85ED-F796B9B71EC6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f03fa07ea56921989d471d9c88f2bffd97e8f98","datavalue":{"value":"6286088","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$AD653C95-C1E0-4F9C-A1AD-29D50E37302F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5410477$33553821-C921-4647-BC02-3C53E2A90D1E","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":"Q5410477$D9DB1562-697B-47DE-B808-FAB28FBA2D5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5410477$48B31AE2-1486-4298-908F-045AAB8EE6D4","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":"Q5410477$60D7EB94-A014-4C71-8F16-DAFF6818E669","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f271ed30a59df5264a928482a64c997dc9b333b1","datavalue":{"value":"https://doi.org/10.1007/978-3-319-06251-8_4","type":"string"},"datatype":"url"},"type":"statement","id":"Q5410477$CD5F1198-A2EE-41CC-938B-2D26EC9A8BC2","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"49a45d1ff3071b498d71ee97a0efe26ed84418b7","datavalue":{"value":"W23903359","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5410477$121F8A66-EF99-4112-959A-DBC5211E14A4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"309c1645d9418ad0e47ec780e6b4f4b7e5af74a1","datavalue":{"value":{"entity-type":"item","numeric-id":5327345,"id":"Q5327345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"719e1a1c29f35eb9b3c1b2002e51d5cd608c1504","datavalue":{"value":{"amount":"+0.8400439023971558","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":"Q5410477$228D9DE8-6F68-4B67-B6D3-305669A3361D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c7fa3d3d0eea70a1a135949962f4363d5f425c8a","datavalue":{"value":{"entity-type":"item","numeric-id":1881265,"id":"Q1881265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1e34ca1f4276d45c1bf9816464dccd9436c6d36","datavalue":{"value":{"amount":"+0.8285529613494873","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":"Q5410477$27F4B3C0-0980-43CC-B6B3-D354213DC858","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15529d64dbf61a436024a0579129e429bcf78898","datavalue":{"value":{"entity-type":"item","numeric-id":4808696,"id":"Q4808696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac9e89911b55e837365139469508e3c9e4b87a8d","datavalue":{"value":{"amount":"+0.8180786371231079","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":"Q5410477$EFDC9E0F-2021-46E3-9E8D-792EFD7551AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2618efea89b8ac42f420f233d84c1b7796adac0c","datavalue":{"value":{"entity-type":"item","numeric-id":2281640,"id":"Q2281640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a27f28eeaaf866cc9f54d397749d5d65c2e0bcf","datavalue":{"value":{"amount":"+0.8174165487289429","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":"Q5410477$F4E5620F-288D-4FF6-A00E-F1E5B76F3182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ad1c15c67b1d1d844274756cd37d1eb7d789969","datavalue":{"value":{"amount":"+0.8154926300048828","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":"Q5410477$2AD77AA6-8CD5-4492-B4CB-F89D3F9B05A7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5410477","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5410477"}}}}}