PVSの使い方 - ATPとCASのこと

今更ですが，使い方です．端末から

pvs

とすると，emacsが起動し

M-x nf

でNew file name:と尋ねられ，例えばdemoe20160519と適当に入力すれば，demo20160519.pvsが

demo20160519  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  

  END demo20160519

のような初期内容で生成されます．そこで，例えば

demo20160519  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
A:TYPE+
a:A
x,y:var A
p:[A->bool]
  % ENDASSUMING

f01:lemma exists(x):(p(x)=>(forall(y):(p(y))))
  

  END demo20160519

のように宣言とステートメントと書き込み（type,var,lemmaといった予約語はcase insensitive）

M-x pr

とすれば

Installing rewrite rule sets.singleton_rew (all instances)


f01 :  

  |-------
{1}   EXISTS (x): (p(x) => (FORALL (y): (p(y))))

Rule?

のような＊pvs＊バッファが開くので，以下のように順次入力する（実際には，TABの後に，fでflatten，iでinstなどのバインドを用います．キーバインド一覧はTAB h，また，コマンドの一覧はTABのみの連打，＊pvs＊への復帰はq）と

f01 :  

  |-------
{1}   EXISTS (x): (p(x) => (FORALL (y): (p(y))))

Rerunning step: (inst-cp 1 "a")
Instantiating (with copying) the top quantifier in 1 with the terms:
a,
this simplifies to: 
f01 :  

  |-------
[1]   EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2}   (p(a) => (FORALL (y): (p(y))))

Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
f01 :  

{-1}  p(a)
  |-------
[1]   EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2}   (FORALL (y): (p(y)))

Rerunning step: (skeep*)
Iterating skeep in '*,
this simplifies to: 
f01 :  

{-1}  p(a)
  |-------
{1}   EXISTS (x): (p(x) => (FORALL (y): (p(y))))
{2}   (p(y))

Rerunning step: (inst 1 "y")
Instantiating the top quantifier in 1 with the terms: 
 y,
this simplifies to: 
f01 :  

[-1]  p(a)
  |-------
{1}   (p(y) => (FORALL (y): (p(y))))
[2]   (p(y))

Rerunning step: (flatten)
Applying disjunctive simplification to flatten sequent,
Q.E.D.

となり，先のバッファに戻るので，ポインターをf01上に置き

C-c 2 p

とすれば

demo20160519  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
A:TYPE+
a:A
x,y:var A
p:[A->bool]
  % ENDASSUMING

f01:lemma exists(x):(p(x)=>(forall(y):(p(y))))

%|- f01 : PROOF
%|- (then (inst-cp 1 "a") (flatten) (skeep*) (inst 1 "y") (flatten))
%|- QED
  

  END demo20160519

のようにプルーフスクリプトが書き込まれます．手を加えたい場合は，先度，M-x pr，もしくは直接

%|- f01 : PROOF
%|- (then (inst-cp + "a") (flatten) (skeep*) (inst + "y") (flatten))
%|- QED

のように書き換え，ポインターをスクリプト上に置き

C-c ! p

とすれば，インストールされます．なお，コメントアウトには，C-c ; が使えます．

また，＊pvs＊上での一般の操作でよく用いるのは

クイットは，q，または，C-z z
（grindが帰ってこないときなどに便利な）インタラプトは，C-c C-c
で，LISPに入ってしまった場合の復帰は，(restore)
コマンドの前後に括弧を付して実行は，C-j
コマンド履歴は．M-s，または，C-上下矢印

辺りでしょう．