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

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



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