{"entities":{"Q7361573":{"pageid":31520258,"ns":120,"title":"Item:Q7361573","lastrevid":105423686,"modified":"2026-10-08T13:45:36Z","type":"item","id":"Q7361573","labels":{"en":{"language":"en","value":"Differential Game Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Differential_Game_Logic"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5f92331a4dfe272ecfe4cae260035b032244a3e5","datavalue":{"value":"https://isa-afp.org/entries/Differential_Game_Logic.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361573$911D57A9-0493-435D-ABFF-C197D961C9CD","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"2b48e2682a2513a0cff9334966950be891f3a311","datavalue":{"value":"Andr\u00e9 Platzer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361573$F3C1359E-D462-4973-A292-F1D96C4B5706","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"62d1caed7d9dc1fd21a18d3ac5d0fbc8eaaf5274","datavalue":{"value":"This formalization provides differential game logic (dGL), a logic for proving properties of hybrid game. In addition to the syntax and semantics, it formalizes a uniform substitution calculus for dGL. Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. The uniform substitutions for dGL also substitute hybrid games for a game symbol everywhere. We prove soundness of one-pass uniform substitutions and the axioms of differential game logic with respect to their denotational semantics. One-pass uniform substitutions are faster by postponing soundness-critical admissibility checks with a linear pass homomorphic application and regain soundness by a variable condition at the replacements. The formalization is based on prior non-mechanized soundness proofs for dGL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361573$ECBDE259-225E-4CA7-A3A4-D9D08A4A6DA2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e290955ee6ca5554084d23c314e7b9e86cc94b02","datavalue":{"value":{"entity-type":"item","numeric-id":1651606,"id":"Q1651606"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$07808D6E-BF22-4CD7-9D0C-6B938B8FE9F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a01d623cdb30dd4d047f4e0d4b381cc0d2f01397","datavalue":{"value":{"entity-type":"item","numeric-id":1799081,"id":"Q1799081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$0A92714B-D3C4-4E25-87BE-0887C0276310","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9010deb8721d3089768234610be326b6fe8b0b13","datavalue":{"value":{"entity-type":"item","numeric-id":2305431,"id":"Q2305431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$BEBE0EB1-5283-4219-8EFF-107B4B2B520B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d369a00a912276bbb6f1d71c301f7df62056f0c","datavalue":{"value":{"entity-type":"item","numeric-id":5277902,"id":"Q5277902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$4A1157A6-0F1D-4286-934A-84D1A84E0B44","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9294cebbc147bfa1be1bf0fac1781c80c4b77b1f","datavalue":{"value":{"time":"+2019-06-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361573$CA119406-C747-48C9-A0DA-C32E07047373","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9176918d8f110e3521a94bdf81deaabb79a21556","datavalue":{"value":{"text":"Differential Game Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361573$D9F3739D-9E41-464C-A866-2787CF2DCF67","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":"Q7361573$3AAF9CCE-A6E6-41C8-8B49-8C61744D738F","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aa8f6bd5a2b4440f838b34acf103bdf45fee4f56","datavalue":{"value":{"entity-type":"item","numeric-id":7360797,"id":"Q7360797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$C220C9D2-5E61-42B4-8F59-BAAB45A63BED","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":"Q7361573$F0812396-3926-4AE0-A307-54C727E1EF03","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"7cd1d9d5053c4cbb0070e62dd589d38783ad8676","datavalue":{"value":"32245","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361573$87ADF73B-9101-4689-9B9B-127CA84B041C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361573$D24BAC52-1336-4AFB-9E80-A49F1F5A70E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361573$34E78DC3-104D-468D-8597-1AD0E0258B78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca6833d3c12e329e13f5f7a45eb21803ac988009","datavalue":{"value":"91.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361573$BDB1F528-0AAE-4243-B10D-7AC81EAAA0DA","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6ea1daaaad60197d0d83fc7ac701579957406893","datavalue":{"value":{"entity-type":"item","numeric-id":16063,"id":"Q16063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$225BCB98-0F9E-4F7A-A916-D9FF0DBFE0C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"181a8497f7a319d54026dcfccf5a714e5c58403f","datavalue":{"value":{"entity-type":"item","numeric-id":40512,"id":"Q40512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$772E656B-4BBA-4B48-8618-7963E2CECC6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$0274A2A3-D147-42E7-B347-212BD8FB8FD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cf16ca8b4217a77a4217a7973bcd79e35c3e2bb9","datavalue":{"value":{"entity-type":"item","numeric-id":5974121,"id":"Q5974121"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$A0463097-BEE0-44EC-969D-303996091A7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a84cec67941530633e685a8ee56a19ae6a02d7e8","datavalue":{"value":{"entity-type":"item","numeric-id":56258,"id":"Q56258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$C23D3C1F-2751-4C7A-AE1C-475B5AC78CA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$16129F50-71CF-4583-A48D-E94225F42983","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"fef5119cc276a651ea287663b7bbac85166163c6","datavalue":{"value":{"entity-type":"item","numeric-id":37397,"id":"Q37397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$8672674D-FF35-42F0-96A3-972C2B093599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1cca3a32b180baf92e5c1bd6e47c20bc43d7599e","datavalue":{"value":{"entity-type":"item","numeric-id":32996,"id":"Q32996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$E929F4C7-D7EA-4ABC-8E0E-B79496AB9294","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"dbfb5e33d8cb9dbe814515b007e55b6104c2d79a","datavalue":{"value":{"entity-type":"item","numeric-id":24996,"id":"Q24996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$B9D39271-8071-4E3D-9072-3B6954AB7CA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"de0d5159ddc96393b5171ce31ad1e7bb3c965ab1","datavalue":{"value":{"entity-type":"item","numeric-id":25200,"id":"Q25200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$BEE95834-142A-4E7D-874E-0B50CE790CE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"faba020dd5002b435d2295ed59494070f5de5bcd","datavalue":{"value":{"entity-type":"item","numeric-id":39931,"id":"Q39931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$4DFD890C-AC7F-4AFB-B0DA-059989DF0A41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$4F07EA52-44F6-4064-8037-0E3E49A92601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"64ac3263c009877925208395a08445516c179997","datavalue":{"value":{"entity-type":"item","numeric-id":13572,"id":"Q13572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$B280FFA3-AF01-4144-A6D2-120FC0B1034C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"14c9bcf9c514f08bfce65561dbbcf4b9dde98592","datavalue":{"value":{"entity-type":"item","numeric-id":31984,"id":"Q31984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$F28A45BC-D4AC-4844-A221-4DA7D5DA61D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"24c387ececd24fa7a9a4716819d51e1718cd572b","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$B9E2D781-8521-4793-A106-86761052E434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"20f24b35928b1dd8019717de94ed50292b94fae9","datavalue":{"value":{"entity-type":"item","numeric-id":22891,"id":"Q22891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361573$523D2261-5B92-463F-9063-592048648360","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Differential Game Logic (AFP entry Differential Game Logic)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Differential_Game_Logic_(AFP_entry_Differential_Game_Logic)"}}}}}