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

Re: OWL semantics ( with focus on an axiomatization)

From: Leo Obrst <lobrst@mitre.org>
Date: Tue, 06 Aug 2002 19:37:57 -0400
Message-ID: <3D505DD4.3B8AD3E8@mitre.org>
To: Christopher Welty <welty@us.ibm.com>
CC: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, www-webont-wg@w3.org, www-webont-wg-request@w3.org, "Robert E. Kent" <rekent@ontologos.org>

Actually, Robert Kent has attempted to do just that: NOT proof to code, which is
logical specification to increasingly refined specification to targeted, refined
programming code (ala Kestrel). But ontology to ontology, etc., in the SUO IFF.

Again using category theory as does Kestrel Institute's kids/specware, the IEE
Standard Upper Ontology's candidate, IFF or Information Flow Framework (based on
Barwise and Seligman's Information Flow Theory, itself based on category
theory), tries to map ontologies together.

The IFF is more accurately a meta-ontology, seeking  to relate ontology to
ontology, interpretation to interpretation, theory to theory. Yes, it's a bit
complicated, as you might expect. See:  http://suo.ieee.org/IFF/

We might look at this as an attempt at solving our "next" problem: semantically
mapping ontologies.


Christopher Welty wrote:

> 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

Dr. Leo Obrst  The MITRE Corporation
mailto:lobrst@mitre.org Intelligent Information Management/Exploitation
Voice: 703-883-6770 7515 Colshire Drive, M/S W640
Fax: 703-883-1379       McLean, VA 22102-7508, USA
Received on Tuesday, 6 August 2002 19:39:01 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:46 UTC