[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: TENEVA G Ms -NUCLEAR <galina.teneva@opg.com>*Subject*: Re: PVS Problem*From*: John Rushby <rushby@csl.sri.com>*Date*: Mon, 30 Apr 2001 21:25:53 PDT*Cc*: "'pvs-help@csl.sri.com'" <pvs-help@csl.sri.com>*In-Reply-To*: Your message of Fri, 27 Apr 2001 15:37:22 -0400*Sender*: pvs-help-owner@csl.sri.com

Dear Galina, 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, page 105. 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 decision procedures" ) 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*)) (assert)) "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 lemma name. 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. Regards, John Rushby

- Prev by Date:
**PVS Problem** - Next by Date:
**RE: PVS Problem** - Prev by thread:
**PVS Problem** - Next by thread:
**RE: PVS Problem** - Index(es):