[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
cancelling typecheck-prove proof attempts
- To: email@example.com
- Subject: cancelling typecheck-prove proof attempts
- From: Mark Aronszajn <firstname.lastname@example.org>
- Date: Mon, 3 Apr 2000 11:20:17 -0400 (EDT)
- Delivery-Date: Mon Apr 3 08:22:16 2000
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.)
Reusable Software Research Group
Dept. of Comp. Sci. & Elec. Eng.
West Virginia University