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

Re: TCC's

Hi,

Ralph D. Jeffords writes:
   From: "Ralph D. Jeffords" <jeffords@itd.nrl.navy.mil>
   Date: Wed, 2 Aug 2000 16:51:04 -0400 (EDT)
   Subject: TCC's
   
   In response to Joe Hurd's question about whether the unprovable TCC of his
   example will cause problems the answer is definitely YES. The attached
   PVS dump shows how soundness problems can arise even if you never directly
   reference the unprovable TCC's. 
   
I don't understand your argument. There are no soundness problems
in your example, the proof for "prove_anything" and for
"prove_anything_again" is incomplete, so all you achieved is that
you proved anything under the assumption, that an unprovable TCC
holds. 

Bye,

Hendrik

-----------------------------------------------------------------
Hendrik Tews     PhD student  in theoretical computer science
                 at Dresden University of Technology, Germany

Telefon:   	 +49 351 463 8351
e-mail:    	 tews@tcs.inf.tu-dresden.de
www:       	 http://home.pages.de/~tews/
pgp key:         http://home.pages.de/~tews/pgpkey.asc
-----------------------------------------------------------------
References: