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

Re: OWL semantics ( with focus on an axiomatization)

From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
Date: Tue, 06 Aug 2002 20:07:15 -0400
To: welty@us.ibm.com
Cc: www-webont-wg@w3.org
Message-Id: <20020806200715G.pfps@research.bell-labs.com>

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

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

Hmm.  Again this depends on what you mean by a language.

Turing machines accept a language.  It would be possible to `axiomatize' a
logic using Turing machines.  Of course, proving that the result was
correct would be rather difficult.

The core of ML is a language.  I even think that it is a nice, easy to
formalize language.  Using it to axiomatize a logic would be possible.  In
fact, I expect that this has already been done and that the axiomatization
has been shown to be correct.  (Perhaps someone with more knowledge of the
use of ML and related languages in logic could speak up here.)

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

Well, the problem here is that modern processors are extremely complicated.
It should be possible to design a simple, slow processor that could, in
principle, be shown to be correct.  However, even this would probably not
rise to the level of a completely rigourous proof.

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

Oh, of course.  But some languages, e.g., the lambda calculus, are very
simple, and could even be directly implemented in physical devices.

> 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


PS: What is www-webont-wg-request@w3.org doing in the cc line?
Received on Tuesday, 6 August 2002 20:07:29 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 23:04:33 UTC