Assessment of semantics bug: [was: Re: proof bug in semantics]

Hi Pat,

pat hayes wrote:
> 
> Guys, I have to report a slight disaster.

You did the right thing in bringing this to light immediately.

  Trying to respond to Peter's
> suggestion that we should provide a clear rule-based criterion for RDFS 
> inconsistency, and to prove the resulting lemma, I found a serious flaw 
> in the proofs of the RDF and RDFS entailment lemmas.  There just wasnt 
> time to get nice versions of the corrected proofs written out by the 
> publishing deadline, so the 10/10 semantics document has some ugly stuff 
> in its proof appendix, written in a hurry and with parts of it rather 
> sketchy.
> 
> I apologize to the WG for this.

It is not your fault.  I had doubts about going to 2nd last call without 
a complete review of the semantics doc.  I suppressed them, which in 
hindsight was a mistake.

That is life.  The world is not a perfect place, and one of the things 
I'm learning is just how hard it is, even for very clever people, to get 
things like proofs right.  I forget what it was like programming in 
languages that didn't do a lot of checking of the program at compile 
time.  This seems like writing in machine code without even a machine to 
test the code on - all one has is testing by inspection.

  I hope to have really nice proofs done
> by early next week, and they can be editorial tweaks to the final 
> publication version.
> 
> None of this affects the normative parts of the document.

I think we have to assess how to react to this little problemette.

I think we make life more difficult for ourselves, not easier, if we try 
to rush things through before we are really ready.  We should ask 
ourselves whether we still believe we are ready for lc2.

On the one hand:

   - the proofs are informative - they are there to convince ourselves, 
and others, that the claims we make are justified, e.g. with respect to 
the relationship between the entailment rules and the MT.

   - thus W3C process allows for them to be corrected during last call 
without forcing another last call, provided its just the proof thats 
wrong, not the conclusions.

On the other hand:

   - there are bugs in the proofs - we are not done on the semantics 
document and we have not yet addressed all our issues with it.  The 
latest message from Peter suggests we are not done discussing this yet. 
  By that critereon, semantics is not ready for 2nd last call.

Options:

- go ahead with the second last call announcement

- hold off the second last call announcement till we have sorted the 
problems with semantics (how?).

- go ahead with all except semantics?

Brian

Received on Friday, 10 October 2003 07:17:42 UTC