勿論 echo 'thf(nat,type,nat : $tType). thf(z,type,z : nat). thf(suc,type,suc : nat > nat). thf(nat_induction,axiom,( ! [P : nat > $o] : (((P @ z) & (! [N : nat] : ((P @ N) => (P @ (suc @ N))))) => (! [N : nat] : (P @ N))) )). thf(f,type,f …

帰納法のユニファイもお任せです． echo 'thf(nat,type,nat : $tType). thf(z,type,z : nat). thf(suc,type,suc : nat > nat). thf(nat_induction,axiom,( ! [P : nat > $o] : (((P @ z) & (! [N : nat] : ((P @ N) => (P @ (suc @ N))))) => (! [N : nat] :…

という訳で，高階論理自動定理証明界のホープ Satallax の登場です． echo 'thf(type_x,type,x : $tType). thf(type_y,type,y : $tType). thf(f,type,f : x > y). thf(gl,conjecture, ((! [X1 : x, X2 : x] : (((f @ X1) = (f @ X2)) => (X1=X2))) <=> (? [G…

「高階論理の定理証明システム」という言葉がよく用いられ，実際，主なプルーフ・アシスタントでは高階論理の定理式が扱えます．しかし，それは関数や述語を変数のまま使えるということであり，高階の decision procedure を備えているという意味ではありま…

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

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

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&…