勿論 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 を備えているという意味ではありま…