[Termtools] certification failures

[Carsten Otto]

On Wed, Nov 12, 2008 at 12:14:12PM +0100, Simon Bailey wrote:
> if you want to use the word certification for the process of verifying  
> a proof, you should be aware of the connotations of the word.  
> certification is a boolean process, it either succeeds or fails.  
> compare certification to checksumming a file ? the value is either  
> correct or incorrect, there is no MAYBE in between... same goes for  
> digital signatures (which is the same as certifying something) ? the  
> signature is valid or invalid.

Since certification always succeeds with a result, you are right.
If you, however, do not wait for that result, you cannot know it in
advance. In this case a MAYBE would be the correct answer.

Compare this to TRSs where termination is decidable. If the tool needs more
time to find the proof and a timeout occurs, the answer must not be NO for
terminating examples. This is why we chose the YES/NO/MAYBE triple even
if YES/NO makes more sense in several cases.

> this is the ratification behind my design decision to only include  
> information about success or failure of the certification process.  
> failure to certify/verify a proof within the given parameters should  
> be considered a failure.

It should be a failure with respec to scoring and winning the competition.
It must not be a failure with the meaning "the proofs is incorrect", as
explained above.

Best regards,
-- 
Carsten Otto           otto at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/otto/
RWTH Aachen            phone: +49 241 80-21241
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: Digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081112/d4b33d51/attachment.pgp