Re: OWL semantics

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com>
Subject: Re: OWL semantics
Date: Tue, 6 Aug 2002 12:25:06 +0200

> 
> [...]
> 
> > 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 won't
> > 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.
> 
> Of course not only testing, but lots of theoretical work too.
> Over the past 2300 years many smart people have already done
> lots of sound axiomatisations; no doubt that that will go on.
> 
> -- ,
> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Sure, there have been many sound axiomatisations, and even many complete
axiomatisations, and many correct axiomatisations.  Further, there have
been many axiomatisations that capture intuitions about some logical
concept or formalism without a separate semantics to provide a measure for
correctness.

However, what does that have to do with proving that a large number of
axioms (say, about 140) are correct with respect to a model theory, or even
that they capture the meaning of a complex language (such as OWL)?  To
prove the former requires considerable work - work that can build on
similar efforts in the past, but still new work.  To show the latter also
requires considerable work - work of a very different kind, but still
work.  Will this work have to be done before the WG is finished?  Who will
do it?

Peter F. Patel-Schneider
Bell Labs Research

Received on Tuesday, 6 August 2002 07:19:21 UTC