[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] How to use PVSio for prove formulas?
I read Sam's paper (a Brief Overview of the PVS user interface) and
there is another way to use PVS prover, PVSio.
Is it possible to use PVSio to get the proving results (proved,
unfinished) of propositional formulas?
x1, x2: VAR int
c1: LEMMA (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0)
c2: LEMMA (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)
With this pvs theory, is it possible to do like
% pvsio pvsbatch:c1
% pvsio pvsbatch:c2
In my understanding, some pvsio file (like "pvsbatch_io" which call
"pvsbatch" theory) would be required to do such a thing.
For the example in p 12, "PVSio reference manual", sqrt_newton.pvs,
how can I call the lemma sqrt2 with pvsio (say % pvsio sqrt_newton:sqrt2).
Otherwise I need to generate semantic-attachment for the "pvsbatch"
theory to evaluate each formula via pvsio.
Thanks for your help.