{"entities":{"Q5098720":{"pageid":7128296,"ns":120,"title":"Item:Q5098720","lastrevid":100206965,"modified":"2026-06-05T21:37:00Z","type":"item","id":"Q5098720","labels":{"en":{"language":"en","value":"Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7578341"}},"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":"Q5098720$1FA21E3D-A95D-4A7E-82F0-F79F08C00D83","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"469c3332ffd83b53e550d13a07e4fbdca2f64be1","datavalue":{"value":{"text":"Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5098720$50EAAE60-1F81-4638-9DB3-1185E94D009A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"53fe8bfea08111e9e13c5b1254ed13c650e9b621","datavalue":{"value":"10.1007/978-3-030-43520-2_11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5098720$F0A36FA0-4968-4CDB-B20A-FBC2EFF6078C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6f0d16d56334eda577a220b2d6e48a64c295fa2c","datavalue":{"value":{"entity-type":"item","numeric-id":1617822,"id":"Q1617822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$A7E6C45F-2C98-4507-B47F-1BE60D72A409","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6fa50bb85a8ff3eebc859f9fb68dfa18c6b1e647","datavalue":{"value":{"entity-type":"item","numeric-id":832720,"id":"Q832720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$C69778B3-3C63-4AE9-9EEE-21E0D8831A3E","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":"Q5098720$C0D55706-28EA-46F5-B1E3-D69FB23F777F","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":"Q5098720$45455CA5-3048-45EE-8579-6AAB0F6D4D67","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"24c2eb8fa17c20bdfa5b9ef95dab30ffa7f0677b","datavalue":{"value":{"time":"+2022-08-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5098720$D8987E94-314E-455C-B7A4-00942D5B50C8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"38be3f0518ce605b68caa1c28ffe4838755983b7","datavalue":{"value":"https://arxiv.org/abs/1910.13554","type":"string"},"datatype":"url"},"type":"statement","id":"Q5098720$81FF96DE-4FF7-4E96-91AD-B33EFEE0E245","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"366be6e579972abe0b09d8e870bc59b6907edcf6","datavalue":{"value":"https://eprints.whiterose.ac.uk/155734/1/hybrid_kat.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5098720$8853E240-7918-4412-B391-7E6005311F83","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5098720$99997E2F-3AC6-4E25-A7CD-426CB383A393","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4d3eb091eb573e450d001d633a800a490bbd1205","datavalue":{"value":"7578341","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5098720$E67C922F-5A60-4EE1-BD31-74A10F77FC52","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f60be08d608d0f944d8eadd79e0cf7ce19f7318a","datavalue":{"value":{"entity-type":"item","numeric-id":43914,"id":"Q43914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$E311DCB3-48C8-4CB5-973E-4C971DC8E7A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"21d8e418735efe724052d5393ed9df3f76f76c3d","datavalue":{"value":{"entity-type":"item","numeric-id":40512,"id":"Q40512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$AC78861C-42E8-40B5-8B22-1CE79095ED3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"194a3545ea85ca9d3a7f32da68870ee0fe47a6d0","datavalue":{"value":{"entity-type":"item","numeric-id":43925,"id":"Q43925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$A5ED20E8-7847-4D73-88DA-7CF613561C75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b51aad9f9cb7e5631db9ce3025117af99d637d67","datavalue":{"value":{"entity-type":"item","numeric-id":32996,"id":"Q32996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$9DF9E69B-534E-4152-A0DE-EBFA60854618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d36499124f0c64e36c382ec378e7f3140049a3b8","datavalue":{"value":{"entity-type":"item","numeric-id":43928,"id":"Q43928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$23569845-C0E0-44E6-BAF0-1E7FC6A9C706","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":"Q5098720$525030FD-58CD-44DA-9194-0663CE9DA637","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":"Q5098720$C82EB3EC-4243-4CD6-99D4-3B2D272739B5","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":"Q5098720$73FFEF11-4653-4672-8BCD-8C9FB01B2CA3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"172e17b0a68d3dea6d16a6586e0e4c8b3834c162","datavalue":{"value":"W3014009067","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5098720$282B26E6-91CD-4CF5-BB37-F04E43CE3740","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$466E9055-8226-4BA9-8D8F-89F88230087E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79e807f14dcd5f9ad4f6bbeb1f8ea3c4bbb7d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$B0C72C28-DE1D-4589-9C52-EC3DC57BF41E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"702e4362e1156e8786e389888f7888e6a1526239","datavalue":{"value":{"entity-type":"item","numeric-id":3176388,"id":"Q3176388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$CB72A09B-A166-4B75-9B0D-5C6BBDA3B6A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f404e88145076a43f26a4aff438db1058e55c891","datavalue":{"value":{"entity-type":"item","numeric-id":2296290,"id":"Q2296290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$02450F35-5121-4F1C-A8CC-0E0C5FF8BC34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5981e1168811f3b1a276d506216532fa05a55595","datavalue":{"value":{"entity-type":"item","numeric-id":3179407,"id":"Q3179407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$3FF21BFE-3475-4C79-A1B9-09956389D5BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89fd0f9fd1fa7a2df7613d8bd37ed93de45bc31e","datavalue":{"value":{"entity-type":"item","numeric-id":5278188,"id":"Q5278188"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$9DEA8896-B27E-47FF-83E5-15ACE272E34D","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":"Q5098720$80A30D4D-A94E-406F-B1B8-6914A9B3B452","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab1507b6b5edb70d4c69829a2d7e9cc7ed436f50","datavalue":{"value":{"entity-type":"item","numeric-id":832721,"id":"Q832721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$982FF50D-350C-47BC-9E6F-3795E8A29A80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b6f4b63bc26052368e7b5944153c26fe1fa531","datavalue":{"value":{"entity-type":"item","numeric-id":2914756,"id":"Q2914756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$11959E41-CC5F-4A5E-9C79-CB3B590C88CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6974134b0a79f0a7c99fc8d68a2c66295fb57263","datavalue":{"value":{"entity-type":"item","numeric-id":1722644,"id":"Q1722644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$41AA8727-8F93-49A4-8121-C5B5B5B7B67C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"807ba00199ace6f7367558f06f230d3484fc77af","datavalue":{"value":{"entity-type":"item","numeric-id":4362921,"id":"Q4362921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$ABA0EE8D-97E5-4515-9CB1-F6D16D90AB61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e13d4d25d9b41b80813e9e3772d78e6f24c19a44","datavalue":{"value":{"entity-type":"item","numeric-id":5738898,"id":"Q5738898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$E4A42321-B6E4-4433-A90B-354BD6D8C686","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5ea185342b06e9bf2135c3b9967061e61dbdbd7","datavalue":{"value":{"entity-type":"item","numeric-id":4635909,"id":"Q4635909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$AD054739-E681-4DB2-A5AC-5A0114F014BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62386516d9e4edfd13150a63c443c59cb377920e","datavalue":{"value":{"entity-type":"item","numeric-id":820135,"id":"Q820135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$4022B35C-CEDB-411B-9CCC-4B5112784A18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"768da93377b5dbe67ffc466d796d0d32932c2d63","datavalue":{"value":{"entity-type":"item","numeric-id":4301161,"id":"Q4301161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$33CAE3C9-FF08-4C44-8B63-B0A769716F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f80eaa52138fe6dc1cc5abd1424bc7779edb1d9a","datavalue":{"value":{"entity-type":"item","numeric-id":4689064,"id":"Q4689064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$17ADA3D4-5923-4B76-B40A-9664BBD914E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28f2d549e1b626474f93418690a7f88013a48545","datavalue":{"value":{"entity-type":"item","numeric-id":4640310,"id":"Q4640310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$98C1A912-02A0-468C-88D2-D43AC0A54560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8851fe9a8b74a22f13014c60a93a01c4d96c785","datavalue":{"value":{"entity-type":"item","numeric-id":2897328,"id":"Q2897328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5098720$6044F7DA-B573-4EF6-ADE6-1F58E3601C34","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ac85bd022b060d7065458581496d049a21c00b4","datavalue":{"value":{"entity-type":"item","numeric-id":832721,"id":"Q832721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5ab37738c30d00f95b70c824114ba25998e5ad30","datavalue":{"value":{"amount":"+0.8476543426513672","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":"Q5098720$73F921CA-701A-4F7C-A263-0F68AE4216CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1ec6d937d521fc45490acf8aa503fd3f527780e","datavalue":{"value":{"entity-type":"item","numeric-id":4635909,"id":"Q4635909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"668c53d7ee2340883aab1d4b5cc19c7e9b1ab3f0","datavalue":{"value":{"amount":"+0.842548668384552","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":"Q5098720$282DCE63-3A80-4362-A6CB-153E4EBD9992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1aa1f4841de960501ed36ce114855cf0bd00d78f","datavalue":{"value":{"entity-type":"item","numeric-id":1040772,"id":"Q1040772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70ab639e8ac103dd349d7bd650f672da827661c9","datavalue":{"value":{"amount":"+0.8351874351501465","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":"Q5098720$7E153ED7-5E94-434B-BF06-D4FA43934B76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35521c642e13426dc82fd1ec84ffa70ef0ae3ed9","datavalue":{"value":{"entity-type":"item","numeric-id":1617825,"id":"Q1617825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d532324da618cf2e5a2369f2606c535d9fa2e8fe","datavalue":{"value":{"amount":"+0.820109486579895","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":"Q5098720$EAD65AA0-2D0D-425C-BA9E-2607FA95BA80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f8bf7ec0f3a410a417075a3d76c794495c1ec5d3","datavalue":{"value":{"entity-type":"item","numeric-id":3613026,"id":"Q3613026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0433ef969608fba6f38ceb3e88b0fdf137fd4f7a","datavalue":{"value":{"amount":"+0.8101716041564941","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":"Q5098720$2228DB64-906B-4920-82BC-B17BF559101F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Differential_Hoare_Logics_and_Refinement_Calculi_for_Hybrid_Systems_with_Isabelle/HOL"}}}}}