Interaction with Prover

• From the command line: pvs
• Change context: C-c C-c
• Create new PVS file: M-x nf
• Type Check: M-x tcp
• Show type correctness conjectures: M-x tccs
• pretty print expanded: C-c C-p e
• Prove a Conjecture:
• Prove the whole file: C-c C-p f
• View prelude file: M-x vpf
• View proof status: M-x spf
• Display the proof in progress: M-x show-current-proof

ProofLite scripts can be created from proofs in two ways: (1) Place the cursor on the formula for which you want to create a ProofLite script and issue the Emacs command: M-x insert-prooflite-script (C-c 2p). T he ProofLite script is automatically inserted after the formula. (2) Issue the command: M-x display-prooflite-script (C-c dp) and enter the name of a formula. The ProofLite script of that formula is displayed in the buffer “ProofLite”.

• Introduce all types in formula: (all-typepreds)
• (typepred a b c)