Re: OWL semantics

On August 6, Jos De_Roo writes:
> 
> [only a very partial reply]
> 
> [...]
> 
> > It is also worth pointing out that such axiomatisations are invariably
> > large and complex, and that it is difficult/impossible to be sure that
> > they are correct. E.g., take a look at the axiomatisation of
> > DAML+OIL/RDF in [3], which contains around 140 axioms. FOL reasoners
> > can be used to detect "obvious" inconsistencies (as happened with
> > earlier versions of [3]), but simply ironing these out is a LONG way
> > from proving that the axiomatisation correctly captures the meaning of
> > the language.
> 
> that is not enough to suggest a
>   "impossible to be sure that they are correct"
> let's just call it difficult/challenging
> engineering and no more

We have invested a lot of time in discussing OWL Lite on the grounds
that the full language would be too difficult for many implementors to
deal with. Can you imagine the conversation with one of these
implementors:

Implementor: Where is the specification of the semantics?

OWL guru: We believe that the intended semantics of the language is
captured in this large set of axioms.

Implementor: You believe?

OWL guru: Yes. Proving that they really do capture the intended
semantics is a difficult/challenging engineering problem.


Moreover, I would be interested in your suggestions as to how one
might go about proving that such an axiomatisation is correct. As you
refer to engineering, I presume that this means testing. Testing wont
PROVE anything (there are infinitely many possible inputs), it can
only show that you didn't find any errors yet. In fact, given that the
axiomatisation is in FOL, which is undecidable, even inputs that would
in principal lead to errors may not reveal anything due to
incompleteness in the FOL reasoner.

Regards, Ian


> 
> -- ,
> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Tuesday, 6 August 2002 05:21:20 UTC