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

Re: [PVS-Help] Proving individual formula in batch mode



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