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.

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.)


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?

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)))))

-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Wednesday, 18 April 2001 21:48:09 UTC