Email Gateway (Aug 22 2022 at 20:04): Email Gateway (Aug 22 2022 at 20:04):From: Manuel Eberl <eberlm@in.tum.de>
Differential Game Logic
by André Platzer
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.
https://www.isa-afp.org/entries/Differential_Game_Logic.html
Enjoy,
Manuel
Last updated: Apr 26 2024 at 04:17 UTC