[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: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