Relational Differential Dynamic Logic
199
where v 0 etc. denote the initial values. Unfortunately, we cannot express exponentiations and logarithms in KeYmaera X, and thus the “solve” rule that we
used in Example 10 cannot be applied here.
One obvious solution to this would be to add support for exponentiations
and logarithms in KeYmaera X, but this would break the decidability of the
underlying first order logic, which is a major feature of dL [18]. In fact, the same
issue occurs even in standard use cases of KeYmaera X, and motivated the
introduction of proof rules which do not demand explicit solutions to differential
dynamics [20,22] using the Lie derivative.
Definition 12 (formal Lie derivative in dL from [20,22]). The formal Lie
derivative of a term f along dynamics δ ≡ ( ˙
x = e & Q) of dimension n is a dL
term L δ f ∈ T (V) given by
6
L δ f :=
∂
∂x1 f · e 1 + · · · +
∂
∂xn f · e n
Definition 13 (proof rules from [20,22]). The following rules are sound:
Γ, Q f ∼ 0 Γ
δ
L δ f 0
Γ
δ
f ∼ 0
DI
Γ p ∼ 0 Q L δ p g · p
Γ
δ
p ∼ 0
Dbx
where δ ≡ ( ˙
x = e & Q), (∼, ) ∈ { (=, =), (>, ≥), (≥, ≥) }, and g is any term
without division.
The differential invariant rule (DI) is the central rule for proving safety properties [20,22]: it reduces a global property of the dynamics to local reasoning by
means of Lie derivatives. The Darboux inequality rule (Dbx) is derived from real
algebraic geometry; see e.g. [22].
Example 14. Consider an example differential dynamics in one variable, ˙
x =
2. Suppose we want to show that x ≥ 0 holds after following these dynamics
for any amount of time, starting from x = 1. One way to do this is to show
that (1) this predicate holds initially and (2) the time derivative of x is always
nonnegative. These are precisely the two premises of the (DI) rule: to show the
sequent x = 1 [ ˙
x = 2]x ≥ 0 (DI) requires us to prove (1) x = 1 x ≥ 0 and
(2) x = 1 [ ˙
x = 2]L ˙
x=2 x ≥ 0, where L ˙
x=2 x = 2. Note that we give an initial
condition x = 1 in the precedent of this sequent.
4 Synchronizing Dynamics
The intuitive explanation of the RDD construction of Definition 9 is a “serialization” of two dynamics. This construction however does not match the (DI)
6 It is easy to see that the derivative of a term t ∈ T (V) with respect to x ∈ V can be
given as a dL term
∂
∂x
e ∈ T (V) such that
∂
∂x
e
=
∂
∂x
e
. The definition of
∂
∂x
e is
inductive with respect to the term e.
199
where v 0 etc. denote the initial values. Unfortunately, we cannot express exponentiations and logarithms in KeYmaera X, and thus the “solve” rule that we
used in Example 10 cannot be applied here.
One obvious solution to this would be to add support for exponentiations
and logarithms in KeYmaera X, but this would break the decidability of the
underlying first order logic, which is a major feature of dL [18]. In fact, the same
issue occurs even in standard use cases of KeYmaera X, and motivated the
introduction of proof rules which do not demand explicit solutions to differential
dynamics [20,22] using the Lie derivative.
Definition 12 (formal Lie derivative in dL from [20,22]). The formal Lie
derivative of a term f along dynamics δ ≡ ( ˙
x = e & Q) of dimension n is a dL
term L δ f ∈ T (V) given by
6
L δ f :=
∂
∂x1 f · e 1 + · · · +
∂
∂xn f · e n
Definition 13 (proof rules from [20,22]). The following rules are sound:
Γ, Q f ∼ 0 Γ
δ
L δ f 0
Γ
δ
f ∼ 0
DI
Γ p ∼ 0 Q L δ p g · p
Γ
δ
p ∼ 0
Dbx
where δ ≡ ( ˙
x = e & Q), (∼, ) ∈ { (=, =), (>, ≥), (≥, ≥) }, and g is any term
without division.
The differential invariant rule (DI) is the central rule for proving safety properties [20,22]: it reduces a global property of the dynamics to local reasoning by
means of Lie derivatives. The Darboux inequality rule (Dbx) is derived from real
algebraic geometry; see e.g. [22].
Example 14. Consider an example differential dynamics in one variable, ˙
x =
2. Suppose we want to show that x ≥ 0 holds after following these dynamics
for any amount of time, starting from x = 1. One way to do this is to show
that (1) this predicate holds initially and (2) the time derivative of x is always
nonnegative. These are precisely the two premises of the (DI) rule: to show the
sequent x = 1 [ ˙
x = 2]x ≥ 0 (DI) requires us to prove (1) x = 1 x ≥ 0 and
(2) x = 1 [ ˙
x = 2]L ˙
x=2 x ≥ 0, where L ˙
x=2 x = 2. Note that we give an initial
condition x = 1 in the precedent of this sequent.
4 Synchronizing Dynamics
The intuitive explanation of the RDD construction of Definition 9 is a “serialization” of two dynamics. This construction however does not match the (DI)
6 It is easy to see that the derivative of a term t ∈ T (V) with respect to x ∈ V can be
given as a dL term
∂
∂x
e ∈ T (V) such that
∂
∂x
e
=
∂
∂x
e
. The definition of
∂
∂x
e is
inductive with respect to the term e.