Re: "equivalentTo" in DAML+OIL

>Richard Fikes wrote:
> >
> > Another issue that emerged from my recent work on a DAML+OIL reasoner is
> > how to deal with the "equivalentTo" property.  I am aware that there has
> > been discussion of "equivalentTo" in the language committee, and I have
> > seen some of those messages.  I would like to add the following comment.
> >
> > It seems that "equivalentTo" enables one to assert that any two
> > resources are equal,
>
>yes...
>
> > meaning that they denote the same object in the
> > domain of discourse.
>
>er... that they _are_ the same object in the domain of discourse.
>
> >  I presume that means "equivalentTo" can be used to
> > assert that any two URIs are equal.
>
>er... that they denote the same resource, yes.
>
> > I am concerned as to what such a general-purpose equivalence property
> > means for reasoners.  It seems on the face of it that DAML+OIL reasoners
> > will need to do full reasoning with equality (using paramodulation?), an
> > unhappy thought.  For example, it seems that if a property has a
> > maxCardinality restriction of 1 at an object and the property has two
> > values V1 and V2 at the object, that a reasoner would need to conclude
> > that V1 is "equivalentTo" V2 rather than concluding that the
> > maxCardinality restriction had been violated.  Is that really what we
> > want?
>
>Well, yes; at least: it's what I want.
>
>But I suspect I'm ignorant
>of a lot of the issues about why this is an "unhappy thought",
>so I'm happy to be educated/persuaded.

Here's why. Equality is easy to understand and pretty easy to 
axiomatize, but it sure plays hell with mechanical searching for 
proofs. Actually the real snag is not really equality as such; it is 
equality plus the lack of a unique-name assumption. As long as you 
can assume that different names name different things, then two 
expressions only have anything to do with one another if they are 
unifiable, which you can test for in close to linear time and then be 
done with. But if different names can co-denote and you are checking 
whether some expression with 'A' in it might mean the same as a 
similar expression with 'B' in it, it's no good just saying that 
since 'A' and 'B' are different, therefore they have nothing to do 
with one another; you have to allow for a new possibility: maybe A=B. 
And now you have to check that A does not =B, and that is a new 
subgoal to prove. So a linear-time trivial syntactic check has 
blossomed into a potentialy infinite subspace search. And this 
happens ALL THE TIME since you keep having expressions which aren't 
unifiable but which could be if only something equalled something 
else, and you have to allow for this possibility (or take the chance 
of missing some proof you might have found if you had been more 
careful.) If terms can equal other terms it gets even worse, since 
who knows? Maybe Fred = the uncle of the first cousin of the father 
of the mother of Diane, and there's another subgoal that you wouldnt 
have had to think about before. Almost anything might be unifiable 
with almost anything else if you allow general equality betwen 
arbitrary expressions. (When equalities can be established by sneaky 
means, as they usually can, the problem gets even worse since it 
tends to leak into the general inference problem.)
Now, y'all in W3C might not care so much about this, since this 
doesnt apply to proof CHECKING since there , presumably, all the 
relevant equalities are stated in the proof itself and then it is 
trivial to check them. The awfulness is when you have to go trying to 
prove their negations, which is like catching rain with a bucket.

>I know a little about co-reference in frame-based
>systems; it's messy...
>
>[[[
>There is a simple theory of coreference  (reasoning
>about whether two frames describe the same object)
>that is no longer loaded by default into the
>knowledge-base. Old examples that use the
>coreference link may fail.
>]]]
>
>--        Helpful Hints
>http://www.cs.utexas.edu/users/qr/algy/reference-manual/node36.html#1010
>Tue, 29 Oct 1996 17:30:00 GMT
>
>and I sometimes manage
>to avoid it in the tools and systems I build,
>but I'm not convinced I want to eliminate
>equality from DAML based on that experience.
>
>
>I've also studied equality in systems
>based on typed lambda calculus, where
>they define "equal" using pages and
>pages of inference rules.
>I'm slowly working my way thru those
>rules. (http://www.w3.org/XML/9711theory/ELF.lsl)
>I sort of understand what's going on,
>but not really.
>
>
>But DAML is specified using pretty straightfoward
>first-order semantics, where I think I have
>a pretty good handle on what "equals" means,
>and it agrees with what most folks learn
>in algebra/gemetry classes in high school,
>if I'm not mistaken.
>
>I don't have a lot of experience building
>reasoners, but I did build one proof checker
>that groks paramodulation
>(http://www.w3.org/2000/10/n3/proofcheck.py)
>and it wasn't hard.
>(well... 'build' is generous; I translated
>McCune's proof checker from a lisp dialect to python.)

Yeh, like I say, proof checking doesnt have to be so worried about 
sizes of search spaces.

>
>By the way... equivalentTo doesn't seem to be the
>only gizmo that introduces equality into DAML:
>UnambiguousProperty, UniqueProperty, cardinality, oneOf,
>etc. all imply equality in various ways, no?
>
>All the axioms that conclude (= ?x ?y)
>are related to this issue, right?

Indeed. Imagine trying to show that (not A=B) with axioms like these around:

>e.g.
>
>Ax63.    (<=> (Type ?p UniqueProperty)
>           (and (Type ?p Property)
>                (forall (?x ?y ?z)
>                        (=> (and (PropertyValue ?p ?x ?y)
>                                 (PropertyValue ?p ?x ?z))
>                            (= ?y ?z)))))
>

Pat Hayes

---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Friday, 20 April 2001 00:58:36 UTC