Re: ISSUE 5.18 Unique Names Assumption Support in OWL

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com>
Subject: ISSUE 5.18 Unique Names Assumption Support in OWL
Date: Wed, 23 Oct 2002 23:04:07 +0200

> 
> Now that all issues are open I'm still feeling
> a bit hesitant w.r.t. issue 5.18
> http://www.w3.org/2001/sw/WebOnt/webont-issues.html#I5.18-Unique-Names-Assumption-Support-in-OWL
> but Frank gave me courage.
> I gathered some experience with something like
> owl:UniqueNames (just gave it some name).
> Let's take an example (which is somewhat crossing
> our charter borders, but it's all I have)
> at http://www.agfa.com/w3c/euler/gedcom
> It is stated there that the gedcom# namespace
> is an owl:UniqueNames meaning that all names in
> that space are actually owl:differentIndividualFrom
> eachother, e.g. all the :... ones in
> http://www.agfa.com/w3c/euler/gedcom-facts.n3
> That is achieved with an inference rule such as
> http://www.agfa.com/w3c/euler/owl-rules#rule10d1
> which implies the ?x owl:differentIndividualFrom ?y
> (instead of giving an order of faculty(n) facts).

Unfortunately this rule won't (or, at least, shouldn't) do anything.  It
says that if x /= y then x and y are different individuals.  Of course, the
whole problem is determining whether x is indeed not equal to y.  The rule
also appears to be doing something illegal with URI references in its use of
log:racine.

On looking at http://www.w3.org/2000/10/swap/log.n3 I realize that the
intended meanings of the resources in the log: namespace are inherently
broken.  For example, log:notEqualTo works on the identifier (URI
(reference)) of its arguments, something completely outside the bounds of
standard logic. 

This brings up a serious problem with the descriptions of CWM.  Sean Palmer
states that CWM is, in some sense, a forward chaining first-order predicate
logic inference engine.   However, if CWM is a reasoner over some logic,
then the logic is a highly unusual intensional logic, and not any standard
first-order logic.

> One can see such inferences in
> http://www.agfa.com/w3c/euler/gedcom-proof.n3
> which is some proof argument for
> http://www.agfa.com/w3c/euler/gedcom-query.n3


> -- ,
> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Peter F. Patel-Schneider

Received on Thursday, 24 October 2002 07:59:37 UTC