solve replaces a (solvable) differential equation x'=f(x)
by an assignment x:=sol(t)
to its solution sol(t)
at time t
along with a quantifier for time t≥0
.
Evolution domain constraints q(x)
are handled correspondingly to check that q(sol(s))
was true at all intermediate times 0≤s≤t
.
Invariant techniques are needed for differential equations that have no solutions in (polynomial) real arithmetic. Reasoning by invariants is also often faster.
See also