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

*To*: pvs-help@csl.sri.com*Subject*: PVS proofs in batch mode*From*: "Cesar A. Munoz" <munoz@nianet.org>*Date*: 19 Nov 2003 14:23:05 -0500*Cc*: "Cesar A. Munoz" <munoz@nianet.org>*Sender*: pvs-help-owner@csl.sri.com

Hi, 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 ? Thanks, Cesar -- Cesar A. Munoz H., Senior Staff Scientist mailto:munoz@nianet.org National Institute of Aerospace mailto://C.A.Munoz@larc.nasa.gov 144 Research Drive http://research.nianet.org/~munoz Hampton, VA 23666, USA Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855

- Prev by Date:
**Re: ask for help** - Next by Date:
**Re: PVS proofs in batch mode** - Prev by thread:
**Re: about the recursive process** - Next by thread:
**Re: PVS proofs in batch mode** - Index(es):