{"entities":{"Q7361038":{"pageid":31518653,"ns":120,"title":"Item:Q7361038","lastrevid":105362477,"modified":"2026-10-07T13:34:13Z","type":"item","id":"Q7361038","labels":{"en":{"language":"en","value":"Differential Dynamic Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Differential_Dynamic_Logic"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"908e26cf64245d0114abe05a96009d5718077afd","datavalue":{"value":"https://isa-afp.org/entries/Differential_Dynamic_Logic.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361038$EC708090-8D61-4C07-90D1-951B9B1AB121","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"91d97292c93b66d906344a5cca8790df7a285fdf","datavalue":{"value":{"time":"+2017-02-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361038$83F1C4EF-BBD5-4DAF-A953-5AC51C44A8DD","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"28a2d2178779194d5d58551d9bdf150a1b03061f","datavalue":{"value":"Rose Bohrer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361038$AE1498BD-E73D-444E-B916-68FBDED3F216","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cb91a98ff46f5b5704ba2106e095677dd06db0f3","datavalue":{"value":{"text":"Differential Dynamic Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361038$102A416E-AE34-44E4-AEA2-EE434BE6C010","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7329e2e8787e1255f19990a10c344a6746847885","datavalue":{"value":"We formalize differential dynamic logic, a logic for proving properties of hybrid systems. The proof calculus in this formalization is based on the uniform substitution principle. We show it is sound with respect to our denotational semantics, which provides increased confidence in the correctness of the KeYmaera X theorem prover based on this calculus. As an application, we include a proof term checker embedded in Isabelle/HOL with several example proofs. Published in: Rose Bohrer, Vincent Rahli, Ivana Vukotic, Marcus V\u00f6lp, Andr\u00e9 Platzer: Formally verified differential dynamic logic. CPP 2017.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361038$5736E128-7411-4FE2-8499-B3DFAF825AB8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f293ebffa7635fb3106a8df0dadaea92d38203f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454116,"id":"Q3454116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361038$8AD1EB3D-BC2F-4BE5-8F23-6642FA6405C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb61c5c1ea145b3c800d5c014b2c4590b1c48513","datavalue":{"value":{"entity-type":"item","numeric-id":1707599,"id":"Q1707599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361038$3E19DADF-2E50-4652-B988-2D1B46373403","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361038$24795647-A19E-4299-9D29-E16B42474BB0","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"eadaad3e8c289407562ca1c737ca67733c4b6104","datavalue":{"value":{"entity-type":"item","numeric-id":7361890,"id":"Q7361890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361038$656CB5D2-4E50-47AB-B572-FD44BD5DA7BA","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"76ebf0a881644521425e5e5631f4667be29e9869","datavalue":{"value":{"entity-type":"item","numeric-id":7360813,"id":"Q7360813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361038$BDFD0E54-E3CA-470B-81F3-EA46461899C3","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361038$882A936C-AB9A-415B-B946-653B9856679A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Differential Dynamic Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Differential_Dynamic_Logic"}}}}}