[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: PVS Problem
1. The commands to automatically apply a specified prover strategy
(grind, by default) to all the theorems in a theory or file are
prove-untried-theory, prut (C-c C-p u) Try untried proofs with given strategy
prove-untried-pvs-file, pruf (C-c C-p U) Try untried proofs with given strategy
I cut and pasted these lines from the PVS help file. There's
additional description in the relevant sections of the PVS User
Guide, starting on page 23.
M-x prut, for example, applies the specified prover strategy to
all the proofs in the given theory that do not already have a
proof. If you've already proved the theorems interactively,
you'll either have to remove the proofs (M-x remove-proof, see
P27) or can just copy the specification to a new theory.
2. The pvs-strategies files are loaded from the current (context)
directory and the user's home directory. See the prover manual,
3. A simple strategy that just calls a succession of other strategies
looks like this
(defstep grnd-repl-assrt ()
(then (ground) (repeat (replace*)) (assert))
"Does GROUND, then REPEAT* (repeatedly) followed by ASSERT"
"Replacing all LHS by RHS and using propositional calculus and
You'd then call this with (grnd-repl-assrt)
The "then" rule just concatenates a number of more basic
strategies. The first string is what's printed by (help
grnd-repl-assrt) and the second is what's printed during a proof.
A simple one that takes an argument is the following.
(defstep use-grnd-repl-assrt (lemma)
(then (use lemma :polarity? t) (ground) (repeat (replace*))
"Uses named LEMMA, then does GROUND, then REPEAT* (repeatedly)
followed by ASSERT"
"Using lemma ~a, Replacing all LHS by RHS and using propositional
calculus and decision procedures"
You'd call this with (use-grnd-repl-assrt "foo") where foo is a
You can look at the definitions of the built-in strategies to see
how more complicated things are done.
The pvs-strategies files are loaded automatically at the beginning
of a proof if the file system indicates they've been changed. You
can force them to be loaded in the middle of a proof by M-x
load-pvs-strategies (see User Guide P27).
Hope this helps you make progress. Please ask again if you need more info.