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

[PVS-Help] How to use PVSio for prove formulas?



Dear helpers,

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?

>> ---
pvsbatch: THEORY

BEGIN

x1, x2: VAR int

c1: LEMMA (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0)
c2: LEMMA (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)

END pvsbatch
>> --

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.

regards,

min