ODE tactic tries to automatically prove differential equation systems [{x'=f(x) & Q}]P
and is especially good at proving invariants.
Complicated cases may benefit from other more dedicated proof rules to obtain faster proofs.
See also
- dI Differential invariant to prove the formula
R
is an invariant of the
differential equation system.
- dC differential cuts: to first prove another property of the differential equation and then assume it during the dynamics.
- dW differential weakening: to prove a property that directly follows from the evolution domain constraint.
- dG differential ghosts: to add a fresh variable with a new differential equation into the dynamics.
Learning resources