[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Time of typechecking
In our work with PVS we have noted the following: when we apply the
command prove-import-chain, we have observed that the time of
typechecking the theory is 2 or 3 times more than the time of proving
the lemmas of the theory.
The reason of this is that the strategies applied to prove TCCs is
bassically grind, while the proofs of lemmas have been optimized by the
user, or there is another reason?