Familiarize yourself with the
PVS Prover Guide,
the
PVS Language Reference
and the
PVS System Guide.
In particular, study the third chapter of the Prover Guide,
which explains the PVS logic and its reasoning rules.
- Instructions:
-
Copy the PVS source files,
A.pvs,
and
B.pvs,
into subdirectory 1 of your homework directory.
-
Move to subdirectory 1
and invoke /usr/local/bin/pvs4.
Using PVS, prove all the theorems in each file.
-
Further instructions, restricting what proof-commands to use,
are included as comments in these source files.
- Notes and Hints:
-
During PVS start-up you may see a message PVS asking whether it should
create a context file for this directory.
The context file is a hidden file named .pvs-context.
PVS will also create a subdirectory
PVSBIN
where it keeps binary state information, and files
A.prf
and
B.prf
that record proofs that you have done.
PVSBIN directories are large and
will be recreated if they are absent. So it is good practice to
remove these directories before depositing your homework in the
repository.
-
In lecture, two PVS system commands were used:
- M-x ff opens a PVS source file (.pvs)
- M-x pr initiates a proof of the theorem under the cursor (i.e. open
the PVS proof editor).
-
The instructions in
A.pvs
and
B.pvs
say what prover commands to use to complete the proofs:
-
For
A.prf you may use
only the commands
(SPLIT f)
and
(FLATTEN f) .
Your learning goal should be to know (not guess) which command to use
at a given point in the proof.
-
For
B.prf you may use
only the commands
(SPLIT f) ,
(FLATTEN f) ,
(SKOLEM f name)
and
(INST f t)
Again, you want to get to the point of knowing (not guessing)
which command to use and when.
-
To get help for a prover command, in the PVS menu invoke
help-pvs-prover-command (C-c C-n c), also available
in the PVS→Help menu.
- The prover's quantifier elimination commands are
(It is important to include the quotation marks):
- (INST i "t") instantiates
the for-all (in the antecedent) or there-exists (in the conclusion)
variable in statement i with the term t.
For example,
{-1} (FORALL x: P(x))
|-------
{1} ...
Rule? (inst -1 "f(a)")
{-1} P(f(a))
|-------
{1} ...
Rule?
|
- (SKOLEM i "v") introduces the
skolem constant (dummy name) for the for-all or
there-exists variable in statement i. Example:
{-1} (EXISTS x: NOT P(x))
|-------
{1} ...
Rule? (skolem -1 "A")
{-1} NOT P(A)
|-------
{1} ...
Rule?
|
rev. Mon Jan 7 16:38:09 EST 2008 SDJ