KeYmaera のいう hybrid system とは，自身の状態に応じて設定を変える系のことで，その性質を扱う論理を，差分で表された action が各変数を繰り返しの回数についての関数と見做すことに加え，微分で表された action が各変数を時間についての関数，従って…

KeYmaera が非線形方程式を解かずに結論を得る仕組みは \problem{ini->\[{ode}\]f>=g} に対して，まず，時刻 0 における成立 ini->f>=g を示し，さらに任意の非負の時刻における f'>=g' の成立を正規型の ode を用いてこの結果から導関数を消去，証明する素…