W3C home > Mailing lists > Public > www-webont-wg@w3.org > August 2002

Re: OWL semantics ( with focus on an axiomatization)

From: Deborah McGuinness <dlm@KSL.Stanford.EDU>
Date: Tue, 06 Aug 2002 14:02:26 -0700
Message-ID: <3D503962.6F3DF90E@ksl.stanford.edu>
To: Christopher Welty <welty@us.ibm.com>
CC: jos.deroo.jd@belgium.agfa.com, "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-webont-wg@w3.org, www-webont-wg-request@w3.org



Christopher Welty wrote:

> I'm sure Deborah knows this, but just for the record:
>
> One can not prove that an axiomatization of a semantics of a language is
> "correct", only that it is consistent.  Since there is no hard link
> between the axiomzatization of the semantics and the actual code that
> implements those semantics, there is no way to know if the axioms
> accurately represent the implementation of the reasoner.
>
> In other words, we have a reasoner like Classic implemented with some
> code, let's call this "artifact 1".  Then we have a set of axioms that
> represent the semantics of Classic, let's call this "artifact 2".  We can
> prove that artifact 2 is consisent, i.e. contains no logical
> contradictions, but we can't prove that it is an accurate representation
> of artifact 1 [1]
>

I was not precise enough on my use of correctness.  Peter has clarified that
point a bit more in subsequent email.

>
> This is only a minor nit, however.  The goal for us of doing an
> axiomatization of the semantics is to provide some formal and consistent
> guide for implementors as to how their OWL implementations should work,
> and I am 100% behind that.
>

yes agreed.

>
> [1] Of course Specware can address this issue since it can generate code
> as a side effect of the proof, thus providing this connection, however I
> suspect you would not want to use the code that specware generates as your
> reasoner since, as far as I know, it only generates efficient code when
> given a lot of domain-specific constraints.  For general software like a
> reasoner, I would expect it to be pretty inefficient, which is not
> desireable for exptime algorithms.

Just for additional clarification,  i dont think anyone was proposing that we
use the output of specware.
Richard W just used it to help check the axioms.

>
>
> -Chris
>
> Dr. Christopher A. Welty, Knowledge Structures Group
> IBM Watson Research Center, 19 Skyline Dr.
> Hawthorne, NY  10532     USA
> Voice: +1 914.784.7055,  IBM T/L: 863.7055
> Fax: +1 914.784.6078, Email: welty@us.ibm.com

--
 Deborah L. McGuinness
 Knowledge Systems Laboratory
 Gates Computer Science Building, 2A Room 241
 Stanford University, Stanford, CA 94305-9020
 email: dlm@ksl.stanford.edu
 URL: http://ksl.stanford.edu/people/dlm/index.html
 (voice) 650 723 9770    (stanford fax) 650 725 5850   (computer fax)  801 705
0941
Received on Tuesday, 6 August 2002 17:01:32 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:51 GMT