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

*To*: RUSHBY@csl.sri.com*Subject*: Re: pvs question/suggestion...*From*: kolano@cs.ucsb.edu (Paul Z. Kolano)*Date*: Fri, 12 Dec 1997 15:20:07 -0800*Cc*: pvs-help@csl.sri.com

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

- Prev by Date:
**Re: cannot ftp to ftp.csl.sri.com as anonymous** - Next by Date:
**A problem about rule "inst"** - Prev by thread:
**Re: pvs question/suggestion...** - Next by thread:
**questions about pvs...** - Index(es):