# Re: OWL semantics ( with focus on an axiomatization)

From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
Date: Tue, 06 Aug 2002 16:51:30 -0400

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

peter
```
Received on Tuesday, 6 August 2002 16:51:39 GMT

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