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

*To*: pvs@csl.sri.com*Subject*: Re: TCC's*From*: "Ralph D. Jeffords" <jeffords@itd.nrl.navy.mil>*Date*: Fri, 4 Aug 2000 12:30:43 -0400 (EDT)*Cc*: pvs@csl.sri.com*Delivery-Date*: Fri Aug 4 09:30:55 2000

Let me clarify my examples and arguments related to the unprovable TCC of Joe Hurd. I interpreted this question to mean "can you have valid results in PVS if you ignore unprovable TCC's?" As you have pointed out in your note on this matter, sometimes it may be the case that a theorem is valid even though the TCC's are unprovable (particularly in the case when the information is really available, but perhaps a formula needs to be reordered so that dependent information appears beforehand in the context of the generated TCC, and thus the TCC becomes provable). Much more common, as your experience shows (and I heartily agree), the theory with unprovable TCC's is just plain wrong. The point of my examples was simply to show that ignoring unprovable TCC's can lead to unsoundness, even when you do not directly reference the unproven TCC's.

- Prev by Date:
**Re: Type-correctness conditions in HOL** - Next by Date:
**AMN-PROOF Tool** - Prev by thread:
**Re: TCC's** - Next by thread:
**AMN-PROOF Tool** - Index(es):