今更ですが，PVS (Allegro Versions)，Yices1，NASA PVS Library，Hypatheon 各最新版のインストールスクリプトです． sudo apt-get -y install sqlite3 echo "export PVS_LIBRARY_PATH=~/CAS/pvs6/nasalib" >> ~/.bashrc source ~/.bashrc mkdir ~/CAS cd ~…

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 とは，与えられた論理式と等価で，量化子を含まない論理式を得る処理のことですが，…

g `!x. asn (sin x) = pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))` ;; e( GEN_TAC );; e( SUBGOAL_THEN `asn (sin x) = asn (sin (pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) )) )…

g `!(x:int). x <= &101 ==> (?n k. 91 <= k /\ k <= 101 /\ x = &k - &(11 * n))` ;; e( REPEAT STRIP_TAC );; e( SUBGOAL_THEN `?m:num. &101 - x:int = &m` MP_TAC );; e( ASM_CASES_TAC `&101 - x:int = &0` );; e( EXISTS_TAC `0` THEN ASM_SIMP_TAC []…

内容はこれからですが．．． http://youtu.be/kzGdyRruGo8 http://youtu.be/H3-qtqrjUiM http://youtu.be/AhybiY0JHvg http://youtu.be/NMSzj_xjZxI http://youtu.be/IvaNo8eMN-Q http://youtu.be/VE1nTWgB6eM まとめて http://www.youtube.com/watch?v=kzGd…

PVS にはカユイところに手が届く帰納法が色々と用意されています．例えば subrange_inductions[i: int, j: upfrom(i)]: THEORY BEGIN k: VAR subrange(i, j) p: VAR pred[subrange(i, j)] subrange_induction: LEMMA (p(i) AND (FORALL k: k < j AND p(k) IM…

うらなりに見える Yices ですが．．． http://d.hatena.ne.jp/ehito/searchdiary?word=%C3%E6%B4%D6%C3%CD の例です． lem1:lemma A(0)<x & (exists m:x<=A(m)) => (exists n:A(n)</x>

各システムにおける実数の扱いが平明に記されています． http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf

以前 Isar で書いた自然数の分解 http://d.hatena.ne.jp/ehito/20130514/1368492752 の PVS 版です． lem_odd_even:lemma forall(n:nat):(n=0 or exists(x:posint,y:nat):odd?(x) & n=x*2^y) %|- lem_odd_even : PROOF %|- (then (induct "n" 1 "NAT_inducti…

Isar で書くと lemma fixes a b :: "real" shows "(a ≠ 0 ∨ a = 0 ∧ b = 0) = (∃x. a * x = b)" (is "?P = ?Q") proof assume ?P moreover have "a ≠ 0 ==> a * (b / a) = b" by auto moreover have "a = 0 ∧ b = 0 ==> ?Q" by auto ultimately show "?Q" by…

PVS のプルーフマネージャは非常に上手く設計されており，ロジカルな展開で迷うことはまずありません． lem0:lemma forall(a,b:real):(a/=0 or (a=0 & b=0)) <=> exists(x:real):a*x=b %|- lem0 : PROOF %|- (then (skeep) %|- (spread (split) %|- ((then (…

sqrtp:theory begin importing ints@primes, ints@gcd, reals@sqrt lem1:lemma forall(p:int): prime?(p) => (exists(n:posint): p = n * n) => False %|- lem1 : PROOF %|- (then (skeep*) %|- (spread (case "divides (n,p)") %|- ((then (expand "prime?"…

HOL系と異なり，PVS の number system は数学と同じく，サブセットからなっていますので numsys1:lemma forall(a:nat): exists(x:real): x=a numsys2:lemma forall(a:nat): exists(x:rat): x=a numsys3:lemma forall(a:nat): exists(x:int): x=a numsys4:lem…

prob10:theory begin for_a:lemma forall(a:posreal,b:posreal,c:int,m:int,n:int):1 / a + 1 / b = 1 => c <= m * a & m * a < c + 1 => c <= n * b & n * b < c + 1 => c = m * a %|- for_a : PROOF %|- (then (skeep) %|- (spread (case "c < m * a") %|-…

theory prob10 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin lemma for_a: fixes a b :: real and c m n :: int assumes "0 < a" and "0 < b" and "1 / a + 1 / b = 1" assumes "c <= m * a" and "m * a < c + 1" assumes "c <= n * b" an…

定理自体はともかく，an_am_coprime の "0" の証明に even_zero_int 等を持ち出さないあたり，さすが metis といったところでしょう． theory prob01 imports Complex_Main "~~/src/HOL/Number_Theory/Primes" begin fun a :: "nat => int" where "a 0 = 3" …

(grind) は中々です．pvsファイル nnseq:theory begin importing reals@sigma_nat a:[nat->nnreal] n:nat lem01:lemma sigma(0,n,a)>=0 lem02:lemma sigma(0,n,a)=0 => a(n)=0 %|- lem0* : PROOF %|- (grind) %|- QED end nnseq ＊PVS＊バッファ pvs(1160): …

PVS は LK を素直にインプリメントしており，否定は直ちにシーケントの対辺に移されます．これは数についての等式において移項により辺々を和の形に直すことに相当します．また，SUBGOALの導入・証明は，本来の case として (P ∨ ¬P),S ==> T が P,S ==> T …

一般項が分数である数列の和です．NASA製の (grind-reals) が要です．pvsファイル frseq:theory begin importing reals@sigma_posnat lem01:lemma FORALL (n: posnat): sigma(1, n, (LAMBDA (k: posnat): 1 / (k * (k + 1)))) = n / (n + 1) %|- lem01 : PRO…

数学的帰納法の例です． lem002 : |------- {1} FORALL (n: nat, x: real): x ^ n = 0 => x = 0 Rerunning step: (induct "n") Inducting on n on formula 1, this yields 2 subgoals: lem002.1 : |------- {1} FORALL (x: real): x ^ 0 = 0 => x = 0 Rerunn…

と言うわけで，暫くは PVS のことを書きます．PVS はSRI(スタンフォード)で90年代初めより開発が進められている対話的定理証明システムで，LK が素直にインプリメントされており論理記号の消去は極めて平易に行えるのですが，ground，grind，assertといった…