[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
PVS proofs in batch mode
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 ?
Cesar A. Munoz H., Senior Staff Scientist mailto:email@example.com
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