### Abstract

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.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics

### Session Differential_Game_Logic

- Lib
- Identifiers
- Syntax
- Denotational_Semantics
- Static_Semantics
- Coincidence
- USubst
- Ids
- Axioms
- Differential_Game_Logic

## Cite

×

Differential_Game_Logic-AFP

    @article{Differential_Game_Logic-AFP,
      author  = {André Platzer},
      title   = {Differential Game Logic},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Differential_Game_Logic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 24, 2019 : Isabelle2019