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