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

Re: pvs question/suggestion...




thanks for the reply.  In response to:


> > ... I will have a theory that just consists of a bunch of
> > theorems that are not necessarily true and want to use a single
> > command to attempt the proofs of all of them using the same predefined
> > strategy.
> 
> If we understand you correctly, you want a variant of M-x tcp
> that automatically applies a single proof strategy to each formula
> in a theory and quits the proof if the strategy fails to prove the
> formula.  This can be done, but we (Sam) would have to write it.  
> 

I have since found a way to achieve my own version of M-x tcp without
requiring any PVS modifications that I think may be of interest to some
people.  The collection of theorems that I want to prove is automatically
generated by my translator.  In addition to generating the .pvs file for
the theory, I had the translator also generate a .prf file, which for each
theorem "th_n", adds a line:
	(|th_n| "" (my-strategy) NIL)
where my-strategy is whatever strategy I want to use for that particular
theorem.  Here's what one of the automatically generated .prf files might
look like for a theory "test" with 3 theorems:

(|test|
 (|th_a| "" (my-strategy) NIL)
 (|th_b| "" (my-strategy) NIL)
 (|th_c| "" (my-strategy) NIL)
)

Then, when I load the associated .pvs file, I can do a M-x prt and PVS will
sequentially "rerun" the proofs of all the theorems using my-strategy without
requiring any user interaction and at the end will display the results in the
"PVS Status" window.  So the results for the above would be:


 Proof summary for theory test
    Interval_TCC1..........................................proved - complete
    foo_TCC1...............................................unfinished
    th_a...................................................proved - complete
    th_b...................................................unfinished
    th_c...................................................proved - complete
    Theory totals: 5 formulas, 5 attempted, 3 succeeded.


So even though the proof of "th_b" failed, PVS just marked it unfinished
and moved on to th_c.  This technique works particularly well for me, since
the theorems I wanted to do this with were already being automatically
generated, so it was simple to produce the .prf file with the translator.

Anyway, hope this is useful for someone.

--Paul