KeYmaera のこと（５）

KeYmaera のいう hybrid system とは，自身の状態に応じて設定を変える系のことで，その性質を扱う論理を，差分で表された action が各変数を繰り返しの回数についての関数と見做すことに加え，微分で表された action が各変数を時間についての関数，従って，自然数と非負実数の直積を定義域とする実数値関数と見做す点を以って，differential dynamic logic と呼んでいます．

例えば，時刻 0 に 0 であった x に「x<0，x=0，00)，0，z(<0) で s 単位時間だけ増加させる」という処理を n(>=0) 回適用したとき，n に寄らず Abs(x)<=Max(y,-z)*s が成り立つ

\problem{x=0&0\[((?(x<0);v:=y)++(?(x=0);v:=0)++(?(0

という性質を


のように証明してくれます．