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

[PVS-Help] Proving individual formula in batch mode

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: joheriks@abo.fi  www: http://www.abo.fi/~joheriks