[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
I have a problem:
In my current work I have to prove about 100 theorems.
I used to work in an interactive way, typing the corresponding primitive
rules after the prompt "rule?".
After a while, I realized that all these proof strategies for the different
theorems can be generalized in one.
Now I want to create a generalized user-defined strategy (something like
grind, but for our specific theorems) in a file, which file to be started
after the first prompt "rule?" or so.
I looked at the "PVS Prover Guide" (version 2.3), in section 5.5 "Defining
Strategies", there is a very brief and not clear to me explanation (and no
example) how to create pvs-strategies file. I have especially difficulties
to understand the syntax of the content of this file. (I want to use
defstep, but as I don't have required-parameters, shall I leave this field
My questions are:
1) Where the name of the user-defined strategy (galina) in the
pvs-strategies file should be tipped? After the first "rule?" prompt or in
the command line area at the bottom, before starting the proof (before
typing M-x xpr)? Could you send me an example, please how the typed command
should look like?
2) Could you send me more explanation and an example of a
pvs-strategies file (just a simple one), to see how it must be organized.
My "success" at the moment:
-I created a pvs-strategies file in the current context directory.
-I put name - galina of my user-defined stratedy. For strategy expression I
used a simple "try" strategy, which strategy works fine if I type it after
the prompt "rule?).
-When then I start the PVS proof, there is a message: "Error in loading file
-When I typed the user-defined name "(galina)" of the strategy after the
prompt "rule?" , a message from the PVS tool appears "GALINA is not a valid
3) Is this message because of bad syntax of the pvs-strategies or something
else in the installation of PVS tool?
I'll appreciate very much your help. Thanks: Galina