Re: OWL semantics ( with focus on an axiomatization)

Peter,

To my knowledge there is no such proof->code connection for any language 
except what has been done with kids/specware. 

Connecting different axiomatizations is possible only given a reliable 
translation between their representations.  It is a theoretical 
possibility, of course, but in practise introduces more sources of 
unreliability.  Intel used a model checker to prove the 486 floating point 
arithmetic worked....yet as we know it didn't.  The breakdown happened 
during translation.

I basically predicted something like this was bound to happen, because the 
formal V&V crowd had been pushing "formal correctness" without requiring 
that the specification that is validated be the specification that 
actually runs.  Should you have more confidence that 150 axioms more 
accurately represents what something does than 1500 lines of code????

Anyway, this is a major tangent.  I just wanted to prevent the claim that 
having an axiomatization proven consistent tells us anything more than it 
does.

-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





"Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
Sent by: www-webont-wg-request@w3.org
08/06/2002 04:51 PM

 
        To:     Christopher Welty/Watson/IBM@IBMUS
        cc:     www-webont-wg@w3.org
        Subject:        Re: OWL semantics ( with focus on an axiomatization)

 


From: "Christopher Welty" <welty@us.ibm.com>
Subject: Re: OWL semantics ( with focus on an axiomatization)
Date: Tue, 6 Aug 2002 16:42:30 -0400

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

That depends on what you mean by ``correct''.

It is possible to prove that an axiomatization is sound and complete wrt
some other formal specification of entailment, such as a model theory, or
even a different axiomatization. 

> 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]

Why not?  Let's assume that the reasoner for Classic is ``implemented'' in
the lambda calculus, to pick an obvious example.  It is possible, but very
hard, to show that a set of axioms in some formal system corresponds to
this ``implementation''.

Of course, any particular LISP system that runs on a physical computer may
not be a correct implementation of the lambda calculus, so there is no
completely-solid connection between the axiomatization and running code.

[...]

> -Chris

peter

Received on Tuesday, 6 August 2002 17:23:27 UTC