The structure of differential invariants and differential cut elimination

The biggest challenge in hybrid systems verification is
the handling of differential equations. Because
computable closed-form solutions only exist for very
simple differential equations, proof certificates have
been proposed for more scalable verification. Search
procedures for these proof certificates are still rather
ad-hoc, though, because the problem structure is only
understood poorly. We investigate differential
invariants, which define an induction principle for
differential equations and which can be checked for
invariance along a differential equation just by using
their differential structure, without having to solve
them. We study the structural properties of differential
invariants. To analyze trade-offs for proof search
complexity, we identify more than a dozen relations
between several classes of differential invariants and
compare their deductive power. As our main results, we
analyze the deductive power of differential cuts and the
deductive power of differential invariants with
auxiliary differential variables. We refute the
differential cut elimination hypothesis and show that,
unlike standard cuts, differential cuts are fundamental
proof principles that strictly increase the deductive
power. We also prove that the deductive power increases
further when adding auxiliary differential variables to
the dynamics.

@article{DBLP:journals/lmcs/Platzer12,
	pdf = {https://lmcs.episciences.org/809/pdf},
	author = {['André Platzer']},
	title = {The Structure of Differential Invariants
               and Differential Cut Elimination},
	journal = {Logical Methods in Computer Science},
	volume = {8},
	number = {4},
	year = {2012},
	pages = {1-38},
	doi = {10.2168/LMCS-8(4:16)2012},
	keywords = {Proof theory, differential equations,
               differential invariants, differential cut
               elimination, differential dynamic logic
                hybrid systems, logics of programs,
                real differential semialgebraic geometry},
	abstract = {
    The biggest challenge in hybrid systems verification is
    the handling of differential equations. Because
    computable closed-form solutions only exist for very
    simple differential equations, proof certificates have
    been proposed for more scalable verification. Search
    procedures for these proof certificates are still rather
    ad-hoc, though, because the problem structure is only
    understood poorly. We investigate differential
    invariants, which define an induction principle for
    differential equations and which can be checked for
    invariance along a differential equation just by using
    their differential structure, without having to solve
    them. We study the structural properties of differential
    invariants. To analyze trade-offs for proof search
    complexity, we identify more than a dozen relations
    between several classes of differential invariants and
    compare their deductive power. As our main results, we
    analyze the deductive power of differential cuts and the
    deductive power of differential invariants with
    auxiliary differential variables. We refute the
    differential cut elimination hypothesis and show that,
    unlike standard cuts, differential cuts are fundamental
    proof principles that strictly increase the deductive
    power. We also prove that the deductive power increases
    further when adding auxiliary differential variables to
    the dynamics.
  }
}