\(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
From MaRDI portal
Publication:2305408
DOI10.1007/978-3-030-29436-6_6OpenAlexW2969536896MaRDI QIDQ2305408
Publication date: 10 March 2020
Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_6
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
Pegasus: sound continuous invariant generation ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Constructive hybrid games ⋮ Implicit definitions with differential equations for KeYmaera X (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Differential dynamic logic for hybrid systems
- Isabelle/HOL. A proof assistant for higher-order logic
- A complete uniform substitution calculus for differential dynamic logic
- First-order modal logic
- \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
- Towards a Formally Verified Proof Assistant
- Logics of Dynamical Systems
- The Complete Proof Theory of Hybrid Systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- A Brief Overview of HOL4
- Torricelli's Law: An Ideal Example of an Elementary ODE
- A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems
- Differential Equation Axiomatization
- Differential Hybrid Games
This page was built for publication: \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
