では，非線形系の自動処理はどの程度実装されているのでしょう？ まず，変数どうしの積を含む方程式系の評価，つまり，環における prover として，NUM_RING，REAL_RINGがあります（INT_RINGはありませんが，環の構造を提供する関数RINGを用いれば実装可能で…

■ prover ARITH_RULE(: term -> thm = )の:int版，:real版としてINT_ARITH，REAL_ARITHがあるわけですが，それらの特徴は ・代数的な並び替えなら非線形でも扱える # INT_ARITH `!a b a' b' D:int. (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) = (…

今回は，HOL Lightにおける数の体系のお話です． これまでも多くの例で扱ってきたhol_typeが:numであり，これは自然数（非負整数）全体の集合でした．同様に，hol.mlのロードだけで利用できる:int，:realは整数，実数全体の集合であり #use "./Complex/make.…