KeYmaera のこと（３）

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

従って，KeYmaera の位置付けは，定理証明システムではなく

R 上の dynamic logic が使える QE ツールの統合環境

が妥当でしょう．

ただし，version 1.* の頃は様々な分野の基本的な例が付属し，汎用の QE ツールであることが判り易かったのですが，近年は Hybrid system への適用のみが強調されています．