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

Date: Tue, 06 Aug 2002 16:51:30 -0400

To: welty@us.ibm.com

Cc: www-webont-wg@w3.org

Message-Id: <20020806165130U.pfps@research.bell-labs.com>

Date: Tue, 06 Aug 2002 16:51:30 -0400

To: welty@us.ibm.com

Cc: www-webont-wg@w3.org

Message-Id: <20020806165130U.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 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 16:51:39 UTC

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