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

[Cesar Munoz <munoz@xxxxxxxxxx>]

Dear Min,

PVSio is an interface to the PVS ground evaluator, not to the theorem  
prover. For example, it allows you to evaluate, either interactively  
via M-x pvsio or in batch mode via the command line utility pvsio, PVS  
ground expressions like "even?(fibonacci(10))".

It seems to me that what you are looking for is ProofLite (http://research.nianet.org/~munoz/ProofLite 
), which provides, among other things, a batch mode interface to the  
PVS theorem prover via the command line utility proveit.

Assuming that you have already proven pvsbatch, you can simply type:

$proveit pvsbatch
Processing ./pvsbatch.pvs. Writing output to file ./pvsbatch.status.
 Proof summary for theory pvsbatch
    c2....................................unfinished           
[shostak](0.02 s)
    Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.07 s)
Grand Totals: 2 proofs, 2 attempted, 1 succeeded (0.07 s)

By default, proveit will display the formulas in pvsbatch that are  
untried, incomplete, or unfinished. However, it also generates the  
file pvsbatch.status with a summary of the results for all formulas:

***
*** File: ./pvsbatch.pvs
*** At: 8:50:30 9/10/2008
*** Generated by: proveit - ProofLite-4.i (09/03/08)
***
 Proof summary for theory pvsbatch
    c1....................................proved - complete    
[shostak](0.05 s)
    c2....................................unfinished           
[shostak](0.03 s)
    Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.08 s)

Grand Totals: 2 proofs, 2 attempted, 1 succeeded (0.08 s)

At this point, I haven't implemented the functionality to prove a  
particular formula in a theory. I will consider this feature in a  
future release. You can, however, generate the proof trace for a given  
formula (in text and in LaTex). For example:
$proveit -t c1,c2 pvsbatch

will generate the files c1.txt and c2.txt containing the proof traces  
of c1 and c2, respectively:

$ more c1.txt

c1 :

  |-------
{1}   FORALL (x1, x2: int): (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0)

Trying repeated skolemization, instantiation, and if-lifting,
 This completes the proof of c1.

Q.E.D.

$ more c2.txt
c2 :

  |-------
{1}   FORALL (x1, x2: int): (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)

Trying repeated skolemization, instantiation, and if-lifting,
c2 :

{-1}   integer_pred(x1!1)
{-2}   integer_pred(x2!1)
{-3}   (x1!1 > x2!1)
{-4}   (x1!1 > 0)
  |-------
{1}   (x2!1 > 0)

 Postponing the proof of c2.

Finally, if the file pvsbatch was generated mechanically, ProofLite  
provides a notation to attach, in batch mode, proofs to formulas. For  
instance, the line "%|- c* : PROOF (grind) QED" is a ProofLite script  
that attaches the proof step (grind) to all formulas that match c*.

pvsbatch: THEORY

BEGIN

%|- c* : PROOF (grind) QED

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

The proveit command automatically understands ProofLite scripts.

There are many other features in ProofLite that you may find useful.  
If you are interested, I would recommend looking at the documentation  
available in http//research.nianet.org/~munoz/ProofLite.

Hope that this helps,
Cesar


On Sep 9, 2008, at 9:05 PM, Kyongho Min wrote:

> 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

Cesar Munoz (NIA)
munoz@xxxxxxxxxx