[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: PVS proofs in batch mode
It is possible to write a strategy by indexing off the lemma
name. Strategies can access all of the data structures.
In particular, the *top-proofstate* global contains a proof state
whose label field contains the id corresponding to the lemma, and
the rerun strategy can be used to run a proofscript.
I'm happy to write such a strategy if needed.
> From: "Cesar A. Munoz" <firstname.lastname@example.org>
> Subject: PVS proofs in batch mode
> Date: 19 Nov 2003 14:23:05 -0500
> To: email@example.com
> Cc: "Cesar A. Munoz" <firstname.lastname@example.org>
> Is there a way to associate script proofs to lemmas in batch mode ?
> The long version of the question is: Assume that I have automatically
> generated a PVS theory file with lemmas lem_1,...,lem_n (n is somehow
> big). Assume that I know how to generate proof scripts for each one of
> the lemmas, let say ps_1, ...., ps_n. Is there a quick and simple way to
> associate the proofs scripts to the lemmas (ps_1 to lem_1,...,ps_n to
> lem_n) by running PVS in batch mode ?