KnxmWiki には長所のような書き方をしましたが，外部のツールをバックエンドに用いることは，理論の公理的構成においては致命的です．それはかつて多くの証明系が惑わされた甘美な道ですが，バグを抱えたグラマラスな CAS と心中するのは願い下げなわけで．…

KeYmaera（キメラ）の目玉の一つは 微分方程式系，微分不等式系で表された Continuous evolution を action に使えること ですが，見ての通り \programVariab 以下で，ロジカルな変数が時間の関数なのか否かを明示していません．例えば，先の２つ目の例の時…

http://www.knoppix-math.org/wiki/index.php?KeYmaera に紹介記事を書きましたが，幾つか補足しておきます．差分方程式の例 \programVariables{R x;} \problem{x\[x:=x/2+1*\]x 微分方程式の例 \programVariables{R x,v,a;} \problem{x>=0&a>=0&(v>=0|(a>0&…