一般項が分数である数列の和です．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といった…