[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Proving individual formula in batch mode
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.
(defun my-prove-formula (theoryname formname)
(let ((*suppress-printing* t)
(if (eq (status-flag (prove-formula theoryname formname t)) '!)
(format t "~%Formula proved")
(format t "~%Formula unproved"))))
Johannes Eriksson <firstname.lastname@example.org> 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?
> Johannes W. E. Eriksson, M.Sc.
> Ph.D. Student / Turku Centre For Computer Science (TUCS)
> Åbo Akademi University / Department of Information Technologies
> e-mail: email@example.com www: http://www.abo.fi/~joheriks