(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 …