Source-linked AI summary
A Complete Uniform Substitution Calculus for Differential Dynamic Logic
André Platzer
TL;DR
Differential dynamic logic needs a proof calculus that avoids intricate axiom-schema side conditions and complex prover implementations. The paper uses sound uniform substitutions with differential forms to build a finite, modular axiomatization, and proves it sound and relatively complete while substantially simplifying the soundness-critical prover core.
Problem
Existing dL calculi rely on axiom schemata and proof rules with subtle occurrence, freshness, and variable read/write side conditions that complicate implementation.
Method
The paper uses uniform substitutions and variable renamings derived from static semantics, together with differential forms that internalize differential-equation reasoning as first-class axioms.
Results
The resulting calculus is sound and relatively complete, and KeYmaera X’s soundness-critical core is 2.5% the size of KeYmaera’s core.
Takeaways & Limitations
Axioms become ordinary formulas and axiomatic rules become formula pairs, enabling a simpler and more modular dL prover implementation.
Takeaways & Limitations
Invariant search still requires foresight to identify an appropriate instantiation, so proof search remains essentially unavoidable.
Abstract
from arXiv · showhide
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.
1 Introduction
The article replaces intricate dL axiom schemata and proof-rule side conditions with a finite, modular axiomatization instantiated by uniform substitutions. Differential forms internalize reasoning about differential equations, yielding a sound and relatively complete calculus designed for simpler prover implementations.
- Motivation: The calculus addresses implementation complexity in existing dL sequent calculi, whose rule schemata require subtle occurrence and variable read/write checks.These constraints make the implementation nontrivial and inflexible in KeYmaera.
- Uniform substitution calculus: Uniform substitutions instantiate predicate and function symbols while respecting dL’s binding structure through definitions derived from static semantics.This lets proofs start from a dL formula that is an axiom, with admissibility enforced by the substitution framework.
- Uniform substitution calculus: Uniform substitutions replace soundness-critical schema variables and occurrence side conditions with concrete object-level axioms and axiomatic rules.The approach confines language-dependent static-semantics knowledge to uniform substitutions and variable renamings.
- Differential forms: Differential forms internalize differential invariants, cuts, ghosts, substitutions, total differentials, and Lie derivatives as separate first-class axioms.They support axiomatic reasoning about differential equations and differentials within dL.
- Results: The resulting modular calculus is proved sound and relatively complete, while its axioms and axiomatic rules reduce prover implementation to uniform substitutions and reusable formulas.The paper presents separate soundness arguments for the static semantics, substitutions, axioms, and differential-form reasoning.
2 Differential-Form Differential Dynamic Logic
This section extends differential dynamic logic with differential forms and develops the static semantics needed to support sound uniform substitutions. It defines the syntax and semantics of hybrid programs, then establishes coincidence and variable-change properties that underpin the calculus.
- 2.1 Syntax: Differential-form dL uses independent differential symbols and term differentials so derivatives can be interpreted from state values while differential equations constrain their evolution.Variables include differential symbols such as x′, and differential equations give x′ its time-derivative meaning along an evolution.
- 2.1 Syntax: Differential forms add term-level differentials, enabling differential-equation reasoning to be internalized as local equations of differentials.The differential (θ)′ depends on how θ changes through its free variables and corresponding differential symbols.
- 2.1 Syntax: dL formulas combine arithmetic comparisons, predicate and quantifier symbols, Boolean connectives, quantifiers, and modalities expressing properties after all or some program runs.The modalities [α]φ and ⟨α⟩φ quantify over all and some runs of α, respectively.
- 2.1 Syntax: Hybrid programs combine assignments, tests, differential equations with evolution domains, nondeterministic choice, sequencing, and repetition.These constructs are defined by the grammar α,β ::= a | x:=θ | ?ψ | x′ = θ &ψ | α ∪β | α;β | α∗.
- 2.3 Static Semantics: Static semantics establishes bound-effect and coincidence lemmas for programs, terms, and formulas, characterizing which variables can change and which values determine evaluation.The program coincidence lemma also accounts for interpretations and preserves agreement on variables outside the relevant free-variable set.
- 2.4 Correct Static Semantics Computations: Modal free-variable analysis must distinguish variables written on every execution path from variables written only on some paths, motivating must-bound variables.For [x:=1∪y:=2]x ≥1, the initial value of x can still matter because one branch leaves x unchanged.
- 2.4 Correct Static Semantics Computations: The static semantics soundness lemma shows that syntactic bound and free-variable computations safely support the preceding semantic properties and later uniform-substitution soundness.These computations characterize state changes caused by formulas and programs and the state components on which their values and behavior depend.
3 Uniform Substitutions
Uniform substitution recursively replaces symbols in dL terms, formulas, and programs while admissibility prevents free variables from entering bound contexts. The rule is sound and can instantiate locally sound rules, yielding a constructive basis for dL proof calculus implementation.
- Uniform substitution: Uniform substitution simultaneously replaces function, predicate, quantifier, and program symbols with terms, formulas, and hybrid programs, respectively.Arguments are inserted recursively into replacements.
- Admissibility: A substitution can be sound for one formula yet clash for another when its replacement introduces a free variable into a modality that binds that variable.The examples contrast admissible substitution in [y:=f]p(2y) with the unsound clash in [x:=f]p(x).
- Admissibility: Admissibility requires that variables bound by operators are not free in the corresponding substitution replacements; otherwise the substitution clashes and is undefined.This syntactic condition captures the soundness-critical restriction on substitutions.
- Soundness: The soundness proof relates syntactic substitution to an adjoint interpretation that modifies the interpretations of substituted symbols.Under admissibility, the substituted expression has the same semantics in the adjoint interpretation as the original expression.
- Soundness: Uniform substitution is sound, and uniform substitution instances with FV(σ)=∅ of locally sound inferences remain locally sound.The latter result extends instantiation from axioms and valid formulas to proof rules and whole proofs.
4 Differential Dynamic Logic Axioms
The dL axiomatization uses a finite list of concrete formulas and rule pairs instantiated by uniform substitution rather than infinitely many schema instances. Its axioms cover core program and logical constructs, while a Barcan-schema restriction marks a completeness-proof boundary.
- Axiomatization: Uniform substitution reduces dL axioms and proof rules to a finite list of concrete formulas and formula pairs.Soundness is checked for each concrete axiom or rule rather than for all schema instances satisfying side conditions.
- Core axioms and rules: The calculus includes axioms for modality duality, assignments, tests, nondeterministic choice, and sequential composition, alongside generalization, quantification, modus ponens, and congruence rules.These rules express standard compositional principles for hybrid programs and formulas.
- Sound instantiation: Uniform substitution distinguishes sound instantiations from unsound attempts by clashing when a replacement would introduce a free variable into a bound context.The clash mechanism handles binding structures directly, including modalities and differential-equation contexts.
- Completeness boundary: The Barcan schema cannot be included without restricting program access to the quantified variable, because a program may read or write that variable.The unrestricted schema would be unsound for programs such as x:=0 or tests depending on x.
- Completeness boundary: The prior dL completeness proof does not carry over, but a more general differential-game-logic completeness result implies that the Barcan schema is unnecessary.This preserves the possibility of completeness without importing the unsound unrestricted schema.
5 Differential Equations and Differential Axioms
The calculus uses uniform substitutions and differential forms to internalize reasoning about differential equations as a finite, modular set of axioms without schema side conditions. It is proved sound and relatively complete, while supporting invariants, cuts, ghosts, differential substitutions, and differential-equation solving beyond fully solvable systems.
- Differential axioms: Uniform substitutions yield a finite list of concrete differential-equation axioms without schema variables or soundness-critical side conditions.The axioms replace classical schemas that were limited to simple solvable equations and required freshness and solution conditions.
- Differential axioms: Differential forms internalize differential invariants, differential cuts, differential ghosts, differential substitutions, total differentials, and Lie derivatives as first-class axioms.These axioms can prove properties of more general unsolvable differential equations and retain the properties provable using solutions.
- Differential axioms: Figure 3 combines axioms for differential equations with differential equations for computing differential forms.The differential-equation axioms include weakening, cuts, effects, ghosts, and solving constant equations, while differential axioms cover arithmetic operations and composition.
- Example proofs: Lazy uniform-substitution instantiation reduces proof effort for invariant search, although identifying a closing invariant instantiation still requires foresight.The approach postpones invariant instantiation until the proof conditions become clear, but does not eliminate the need for search.
- Example proofs: Axiomatic differential-equation solving also applies when only part of a system has definable solutions, unlike the classical solution-based schema.The construction provides a verified formal proof using differential axioms rather than an unverified differential-equation solver.
- Soundness and completeness: The calculus soundly instantiates axioms and locally sound rules, and is relatively complete for hybrid systems relative to any differentially expressive logic.Its soundness is modular, and the completeness result preserves the proof power of axiom-schema calculi with a parsimonious soundness-critical core.
6 Conclusions
The paper concludes that uniform substitutions yield a simple, modular, sound, and complete dL calculus based on axioms and axiomatic rules. This design substantially simplifies prover implementations while enabling flexible contextual reasoning.
- Uniform substitutions yield a simple and modular dL calculus based entirely on axioms and axiomatic rules.The calculus replaces soundness-critical schema variables and side conditions with formulas, formula pairs, and recursive uniform substitutions.
- Differential forms provide local semantics that reduce differential-equation reasoning to local reasoning about differential inequalities or equations.This local structure is identified as the key ingredient enabling modularity for differential equations.
- Uniform substitutions also enable flexible reasoning through fast contextual equivalence.The paper presents this capability as an almost-free consequence of the uniform-substitution framework.
- The calculus is sound and complete, with prover implementations reducing proof construction to uniform substitutions guided by static semantics.The approach starts from one copy of each axiom and axiomatic rule.
- KeYmaera X’s soundness-critical core is 2.5% the size of KeYmaera’s sequent-calculus core.The comparison is presented as evidence of significantly simpler and more parsimonious implementation.
A Proofs
The proofs rely on classical analytical results concerning gradients, the mean-value theorem, the chain rule, and global uniqueness of differential-equation solutions.
- The proof development uses the gradient of a function as the vector of its partial derivatives when it exists.
- The mean-value theorem supplies an intermediate point whose derivative relates the change in a differentiable function across an interval.
- The chain rule provides the derivative of a composition when the component functions satisfy the stated differentiability conditions.
- The global uniqueness theorem of Picard–Lindelöf guarantees a unique solution for an initial-value problem under continuity and Lipschitz conditions.