let lem2pn = GSYM(SIMP_RULE[REAL_POW_ONE;REAL_MUL_RID;REAL_ARITH`&1 + &1 = &2`](SPECL[`n:num`;`&1`;`&1`]REAL_BINOMIAL_THEOREM));; g`sum (0..m) (\k. &(binom (n,k))) <= sum (0..n) (\k. &(binom (n,k)))`;; e(DISJ_CASES_TAC(ARITH_RULE`m <= n \/…

g`sum (0..2) (\k. &(binom (n,k))) = &(binom (n,0)) + &(binom (n,1)) + &(binom (n,2))`;; e(SIMP_TAC[REAL_ADD_ASSOC;TWO;ONE;ARITH_RULE`0 <= SUC 0 /\ 0 <= SUC (SUC 0)`;SUM_CLAUSES_NUMSEG]);; let lem01 = top_thm ();; g`2 <= n ==> sum (0..2) (\…

g`!n. &1 + &n + &n * (&n - &1) / &2 <= &2 pow n`;; e INDUCT_TAC;; e REAL_ARITH_TAC;; e(SIMP_TAC[pow;REAL]);; e(SUBGOAL_TAC""`&n <= &n * &n`[ALL_TAC]);; e(DISJ_CASES_TAC(SIMP_RULE[GSYM REAL_LE;GSYM REAL_INJ](ARITH_RULE`n = 0 \/ 1 <= n`)));;…

g`!x. &0 <= x ==> !n. &1 + &n * x <= (&1 + x) pow n`;; e(GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC);; e REAL_ARITH_TAC;; e(SIMP_TAC[pow;REAL] THEN ASSUME_TAC(SPEC_ALL REAL_POS));; e(ASM_MESON_TAC[REAL_LE_ADD;REAL_POS;REAL_LE_LMUL;REAL_LE_MUL;…

#use "Multivariate/realanalysis.ml";; #use "Multivariate/derivatives.ml";; g `!p e. p <= &1 ==> &0 < e ==> ?d. &0 < d /\ !x y. &1 <= x /\ &1 <= y /\ y <= x /\ abs(x - y) < d ==> abs(x rpow p - y rpow p) < e` ;; e( REPEAT STRIP_TAC );; e( A…

sledgehammer の HOL Light 版 http://mws.cs.ru.nl/~urban/ha1.ogv (http://mws.cs.ru.nl/~urban/ha1.mp4) http://mws.cs.ru.nl/~urban/2013-07-cicm.pdf http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-cicm13.pdf

現在では Portable Standard Lisp (PSL)，Codemist Standard Lisp (CSL) ともopenになりましたので，気軽に比較できます．最新版 mkdir ~/CAS export CAS=~/CAS cd $CAS svn co http://svn.code.sf.net/p/reduce-algebra/code/trunk reduce-algebra cd ./red…

RedLog のサイトが新しくなりました． http://redlog.dolzmann.de/

今回は以前名前のみを挙げた，初等超越関数についての（全称）不等式系のsymbolicプルーバー metit http://www.cl.cam.ac.uk/~lp15/papers/Arith/index.html をご紹介します．この metit は MetiTarski (Metis + Tarski) という名からも解るように，代数的な…

今回は以前 http://d.hatena.ne.jp/ehito/20110526/1306382983 少し述べた numeric QE プログラム，RSolver http://rsolver.sourceforge.net/ について書きます．一般に QE とは，与えられた論理式と等価で，量化子を含まない論理式を得る処理のことですが，…