A Uniform Substitution Calculus for Differential Dynamic Logic

Abstract

This paper introduces a new 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 rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of nontrivial schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms in dL.

References in corpus (2)

• Essential Convexity and Complexity of Semi-Algebraic Constraints
• A Uniform Substitution Calculus for Differential Dynamic Logic

Cited by in corpus (8)

• A Complete Uniform Substitution Calculus for Differential Dynamic Logic
• The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving
• A Uniform Substitution Calculus for Differential Dynamic Logic
• Formally Verified Next-Generation Airborne Collision Avoidance Games in ACAS X
• Uniform Substitution for Differential Refinement Logic
• Safety Certified Cooperative Adaptive Cruise Control under Unreliable Inter-vehicle Communications
• Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges
• Complete Robust Hybrid Systems Reachability