A differential operator approach to equational differential invariants

@inproceedings{DBLP:conf/itp/Platzer12,
	pdf = {pub/diffop.pdf},
	slides = {pub/diffop-slides.pdf},
	author = {['André Platzer']},
	title = {A Differential Operator Approach to
               Equational Differential Invariants},
	booktitle = {ITP},
	longbooktitle = {Interactive Theorem Proving,
               International Conference, ITP 2012, August
               13-15, Princeton, USA},
	year = {2012},
	pages = {28-48},
	month = {},
	editor = {['Lennart Beringer', 'Amy Felty']},
	publisher = {Springer},
	series = {LNCS},
	volume = {7406},
	doi = {10.1007/978-3-642-32347-8_3},
	keywords = {differential dynamic logic, differential
               invariants, differential equations,
               hybrid systems},
	abstract = {
    Hybrid systems, i.e., dynamical systems combining
    discrete and continuous dynamics, have a complete
    axiomatization in differential dynamic logic relative
    to differential equations. Differential invariants are
    a natural induction principle for proving properties of
    the remaining differential equations. We study the
    equational case of differential invariants using a
    differential operator view. We relate differential
    invariants to Lie's seminal work and explain important
    structural properties resulting from this view.
    Finally, we study the connection of differential
    invariants with partial differential equations in the
    context of the inverse characteristic method for
    computing differential invariants.
  }
}