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

*To*: joheriks@xxxxxx*Subject*: Re: [PVS-Help] Proving individual formula in batch mode*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Tue, 15 Aug 2006 12:48:49 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Johannes Eriksson <joheriks@abo.fi>message dated "Tue, 15 Aug 2006 17:32:14 +0300."*In-reply-to*: <20060815143214.GF24597@xprog25.cs.abo.fi>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20060815143214.GF24597@xprog25.cs.abo.fi>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Johannes, There is a prove-formula function that takes a theory name, a formula name and a rerun? flag. If rerun? is t, it simply reruns the proof, returning the proof state at the end. You can check if it is proved by checking if the status-flag is '!. You can use your own variations of the following definition, which also suppresses the usual prover output. Regards, Sam Owre (defun my-prove-formula (theoryname formname) (let ((*suppress-printing* t) (*printproofstate* nil) (*proving-tcc* t)) (if (eq (status-flag (prove-formula theoryname formname t)) '!) (format t "~%Formula proved") (format t "~%Formula unproved")))) Johannes Eriksson <joheriks@abo.fi> wrote: > Hi list members, > > We are building a small graphical interface to PVS where we produce a > tabular report about the proof status of each formula in a theory. > The .pvs (and possibly .prf) file is first generated on the fly by our > tool, then we run PVS in batch mode and parse the output to produce > the report. > > Now we want to enable the user to re-run the proof of only a single > formula (identified by its name), but I haven't found any suitable > command in the PVS system guide for this. Basically what the (prove) > command does but without user interaction and in batch mode. So, my > question is like that: is it possible to re-run the proof of an > individual formula based on the name of the formula, the theory name, > and/or the filename? > > Cheers, > -- > Johannes W. E. Eriksson, M.Sc. > Ph.D. Student / Turku Centre For Computer Science (TUCS) > Åbo Akademi University / Department of Information Technologies > e-mail: joheriks@abo.fi www: http://www.abo.fi/~joheriks

**References**:**[PVS-Help] Proving individual formula in batch mode***From:*Johannes Eriksson

- Prev by Date:
**[PVS-Help] Proving individual formula in batch mode** - Next by Date:
**[PVS-Help] How to avoid/discharge an Existence TCC for my subtype** - Prev by thread:
**[PVS-Help] Proving individual formula in batch mode** - Next by thread:
**[PVS-Help] PVS Installation Tips for a Windows enabled computer** - Index(es):