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>

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. Leo 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, USAReceived 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
*