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

cancelling typecheck-prove proof attempts

When you ask PVS to typecheck-prove a theory and it turns out that
typechecking generates a ton of TCCs, PVS may end up spending a lot of
time attempting proofs of the TCCs.  Is there a way to tell PVS to forget
about attempting the proofs once its begun?

(I looked at the PVS System Guide, under Typecheck Prove and didn't find
this particular issue addressed.)


Mark Aronszajn
Reusable Software Research Group
Dept. of Comp. Sci. & Elec. Eng.
West Virginia University