Re: PVS batch mode

[Dave Stringer-Calvert <dave_sc@csl.sri.com>]

> To my understanding, PVS batch mode can automatically reprove the
> theorems that have already been proved manually (i.e. with interaction),
> but it cannot automatically prove new theorems that have never been
> proved, right ?

The PVS batch mode can do nearly anything that can be accomplished in
interactive mode - i.e. anything you can reduce to a sequence of emacs
or Lisp commands.

> I've generated hundreds of theorems using C/C++, and I want to use PVS
> to prove them automatically (i.e. not first prove them with interaction
> , and then rerun the proof).  How can I pass the theorems to PVS and
> have them proved? I've read chapter 5 in the manual, but haven't found
> the answers.

There's a short piece of Emacs lisp below.  Put this in the file
"prove-all.el" in the current directory, and replace "test" with the name
of a PVS file that contains unproven theorems.  Then run:

     pvs -q -batch -v 3 -l prove-all.el

and it will attempt (grind) on each unproven theorem and TCC.  I've also
included an example PVS file and example output from the batch processing.

Dave


-------------<prove-all.el>--------------------------------

(pvs-message "Proving all unproven theorems in test.pvs")
(typecheck "test")
(let ((current-prefix-arg t))
  (prove-untried-pvs-file "test" "(grind)"))
(pvs-message "Completed")


------------<test.pvs>-------------------------------------

test: THEORY
BEGIN

  a : theorem  1 < 2

  b : theorem  2 < 3

  c : theorem  3 < 4

  d : theorem  4 < 5

END test


------------<example output>-------------------------------

Loading pvs-load...
Started initializing ILISP
Finished initializing pvsallegro
Loading compiled patch file /project/pvs/pvs2.3/patch2.lfasl
Context changed to /tmp/p/
Proving all theorems in test.pvs
Parsing test
test parsed in 0.00 seconds
Typechecking test
test typechecked in 0.01s: No TCCs generated
Proving untried formula a

a :  

  |-------
{1}   1 < 2

Rerunning step: (GRIND)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.
Proving untried formula b

b :  

  |-------
{1}   2 < 3

Rerunning step: (GRIND)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.
Proving untried formula c

c :  

  |-------
{1}   3 < 4

Rerunning step: (GRIND)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.
Proving untried formula d

d :  

  |-------
{1}   4 < 5

Rerunning step: (GRIND)
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.


 Proof summary for theory test
    a...........................................proved - complete   [O](0.07 s)
    b...........................................proved - complete   [O](0.01 s)
    c...........................................proved - complete   [O](0.02 s)
    d...........................................proved - complete   [O](0.01 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.11 s)

Grand Totals: 4 proofs, 4 attempted, 4 succeeded (0.11 s)
Completed