  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.
