Re: OWL semantics ( with focus on an axiomatization)

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]

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.

[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.

-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

Received on Tuesday, 6 August 2002 16:43:43 UTC