Differences

This shows you the differences between two versions of the page.

--- pvs:prover [2016/08/23 17:03]
jonathan created
+++ pvs:prover [2017/09/14 16:08] (current)
jonathan [Basic]
@@ Line 1: / Line 1: @@
-====== Basic Interaction with Prover ======
+====== Interaction with Prover ======
+===== Basic =====
+  * 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".
+===== Commands =====
+  * Introduce all types in formula: ''(all-typepreds)''
+  * ''(typepred a b c)''

Software Engineering Documentation