A Complete Uniform Substitution Calculus for Differential Dynamic Logic

Abstract

This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundness-critical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this article introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivatives as first-class axioms to reason about differential equations axiomatically. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete.

Long article extending the conference version that appeared at CADE 2015, arXiv:1503.01981

References in corpus (2)

• Differential Game Logic
• A Uniform Substitution Calculus for Differential Dynamic Logic

Cited by in corpus (34)

• Formal Verification of Obstacle Avoidance and Navigation of Ground Robots
• Verifiably Safe Off-Model Reinforcement Learning
• Differential Equation Invariance Axiomatization
• The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving
• Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
• HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification
• Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
• Verifying Switched System Stability With Logic
• Pegasus: Sound Continuous Invariant Generation
• Uniform Substitution At One Fell Swoop
• An Axiomatic Approach to Existence and Liveness for Differential Equations
• An Axiomatic Approach to Liveness for Differential Equations
• Implicit and Explicit Proof Management in KeYmaera X
• Uniform Substitution for Differential Game Logic
• Implicit Definitions with Differential Equations for KeYmaera X (System Description)
• Switched Systems as Hybrid Programs
• Deductive Stability Proofs for Ordinary Differential Equations
• Analytic Estimation of Region of Attraction of an LQR Controller for Torque Limited Simple Pendulum
• Structured Proofs for Adversarial Cyber-Physical Systems
• Uniform Substitution for Differential Refinement Logic
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• Embedding Differential Dynamic Logic in PVS
• Adaptive Shielding via Parametric Safety Proofs
• Constructive Game Logic
• Axiomatization of Compact Initial Value Problems: Open Properties
• A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
• Verification of Autonomous Neural Car Control with KeYmaera X
• From Zonotopes to Proof Certificates: A Formal Pipeline for Safe Control Envelopes
• Complete Robust Hybrid Systems Reachability
• A Deductive Refinement Calculus for Differential-Algebraic Programs
• Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
• Semi-Competitive Differential Game Logic
• The Significance of Symbolic Logic for Scientific Education
• Heterogeneous Dynamic Logic: Provability Modulo Program Theories