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

[PVS-Help] Time of typechecking



Hello,

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?

Thanks,
María-José Hidalgo