2016-05-19から1日間の記事一覧

Empty domain

古典的(?)な一階の古典論理の意味論では,ドメインAは空でないとされ,その理由として,Aが空では,∀x.p(x),つまり「任意のxについて,x∈Aならばp(x)」が真,∃x.p(x)つまり「あるxについて,x∈Aかつp(x)」が偽,したがって,定理式 ∀x.p(x)→∃x.p(x) が偽…

PVSの使い方

今更ですが,使い方です.端末から pvs とすると,emacsが起動し M-x nf でNew file name:と尋ねられ,例えばdemoe20160519と適当に入力すれば,demo20160519.pvsが demo20160519 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % END…

skeep

PVSのskeepコマンドは,本来は x!1 などのように新規に導入すべきスコーレム定数を,衝突がない限り束縛されていた変数と同じ名前で導入してくれます. f1 : |------- {1} (EXISTS (x: A): (p(x))) AND (EXISTS (x: A): (q(x))) => (EXISTS (x: A): (p(x) AN…