### Abstract

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ölp, André Platzer: Formally verified differential dynamic logic. CPP 2017.

### License

BSD License

### Topics

- Logic/General logic/Modal logic
- Computer science/Programming languages/Logics

### Session Differential_Dynamic_Logic

- Ids
- Lib
- Syntax
- Denotational_Semantics
- Axioms
- Frechet_Correctness
- Static_Semantics
- Coincidence
- Bound_Effect
- Differential_Axioms
- USubst
- USubst_Lemma
- Uniform_Renaming
- Pretty_Printer
- Proof_Checker
- Differential_Dynamic_Logic

### Depends on

- Ordinary Differential Equations

### Auto-related entries

- Abstract Interpretation of Annotated Commands

## Cite

×

Differential_Dynamic_Logic-AFP

    @article{Differential_Dynamic_Logic-AFP,
      author  = {Rose Bohrer},
      title   = {Differential Dynamic Logic},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Differential_Dynamic_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 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Feb 14, 2017 : Isabelle2016-1