∀，∃を消去するには，仮定と結論を分離し，十分条件などに帰着させる方法が一般的です． # g `(!x. &0<x ==> a<x )==> a<= &0` ;; Warning: Free variables in goal: a val it : goalstack = 1 subgoal (1 total) `(!x. &0 < x ==> a < x) ==> a <= &0` # e( STRIP_TAC );</x></x>…

古典論理での〜の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります． 〜Ａ|- |-〜Ａ −−−− −−−− |-Ａ Ａ|- (UNDISCH o NOT_ELIM) |-Ａ Ａ|- −−−− −−−− 〜Ａ|- |-〜Ａ NEG_DISCH,(NOT_INTRO o DISCH) # ARITH_RULE `~(n<0)`;; val it : thm = |…

関数 g で始まる HOL Light の対話的証明作成では，論理式 ~(A0) ∨ … ∨ ~(An) ∨ B が定理式であること，つまり [A0] … [An] A0,..,An |- B あるいは B を 0 [A0] ……… n [An] B と表示します．・HOL Light のプルーフマネージャーは証明を遡って作成しますの…

∧の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります． |- |- ∧|- |-∧ −−−−−−−− −−−−− |- |- |- LCE CONJUNCT1,CONJUNCT2,CONJ_PAIR,CONJUNCTS |- または |- |- |- −−−−−−−−− −−−−− ∧|- |-∧ ADD_ASSUM,LCI CONJ # let LCE th1 th2 th12 = PRO…

Revision: r154 で新規実装された４つのTactic HYP DESTRUCT_TAC FIX_TAC INTRO_TAC は（鶏風ではありますが）ラベリングには便利です．例えば，GEN_TACやDISCH_TAC，DISJ*_TACの働きを有するのが INTRO_TAC http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/…

∀の導入（INTRO）と消去（ELIM）の推論には，以下の４通りがあります．ただし，全称，特称はメタのものです． |-全称 ∀|- |-∀ −−−−−−−− −−−− |- |-全称 LAE SPEC,SPECL 特称|- |-全称 −−−− −−−− ∀|- |-∀ LAI GEN,X_GEN ・古典論理では，対角の推論どうしは，…

インストールスクリプトを書きました．プラットフォームは http://d.hatena.ne.jp/ehito/20130214/1360813508 と同じです．コンパイルには４〜５時間必要です． export CAS=/home/knoppix/CAS cd ~ sudo mkdir ./CAS cd $CAS wget --no-check-certificate ht…

!の定義． FORALL_DEF: `(!) = \P:A->bool. P = \x. T` SPEC `a` `ASM |- !x.P[x]` gives `ASM |- P[a]` SPECL [`a`;`b`;`c`] `ASM |- !x y z.P[x,y,z]` gives `ASM |- P[a,b,c]` SPEC_VAR `ASM |- !x.P[x]` gives (`x17`, `ASM |- P[x17]`) SPEC_ALL repeat…

/\の定義． AND_DEF: `(/\) = \t1 t2. (\f:bool->bool->bool. f t1 t2) = (\f. f T T)` CONJ `ASM1 |- a` `ASM2 |- b` gives `ASM1+ASM2 |- a /\ b` CONJUNCT1 `ASM |- a /\ b` gives `ASM1 |- a` CONJUNCT2 `ASM |- a /\ b` gives `ASM1 |- b` CONJ_PAIR th…

==>の定義． # IMP_DEF;; val it : thm = |- (==>) = (\p q. p /\ q <=> p) MP `ASM1 |- a ==> b` `ASM2 |- a` gives `ASM1+ASM2 |- b` モーダス・ポーネンス． # MP (ASSUME `p==>q`) (ASSUME `p:bool`);; val it : thm = p, p ==> q |- q DISCH `a` `ASM,a…

Tの定義． T_DEF: `T = ((\x:bool. x) = (\x:bool. x))` TRUTH: `|- T` EQT_ELIM `ASM1 |- a = T` gives `ASM1 |- a` EQT_INTRO `ASM1 |- a` gives `ASM1 |- a = T` Fの定義． F_DEF: `F = !t:bool. t` NOT_DEF: `(~) = \t. t ==> F` NOT_ELIM `ASM |- ~a` g…

PINST tyin tmin th instantiates types in th according to tyin and terms according to tmin. # let th = MESON[] `(x:A = y) <=> (y = x)`;; ... val th : thm = |- x = y <=> y = x # PINST [`:num`,`:A`] [`2 + 2`,`x:A`; `4`,`y:A`] th;; val it : th…

紹介したソフトのうち，幾つかのバージョンが上がっていますので，インストールスクリプトを書きました．プラットフォームは http://www.math.kobe-u.ac.jp/vmkm/2012vm/index.html で，新規に導入するものとしますが，手順は http://d.hatena.ne.jp/ehito/2…