From: Christopher Welty <welty@us.ibm.com>

Date: Tue, 6 Aug 2002 17:22:26 -0400

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

Cc: www-webont-wg@w3.org, www-webont-wg-request@w3.org

Message-ID: <OFC351730A.7A68571A-ON85256C0D.00733021@pok.ibm.com>

Date: Tue, 6 Aug 2002 17:22:26 -0400

To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>

Cc: www-webont-wg@w3.org, www-webont-wg-request@w3.org

Message-ID: <OFC351730A.7A68571A-ON85256C0D.00733021@pok.ibm.com>

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 peterReceived on Tuesday, 6 August 2002 17:23:27 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:57:51 GMT
*