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