Re: "equivalentTo" in DAML+OIL

to chime in on the equality issue and to further expand on richard's example,
if we have maximum cardinality of 1 on a term and we have two values (say the
integers 1 and 2),
then we either can determine that
a - 1 is not the same as 2 and thus we have two values and a maximum
cardinality violation
b - or we should determine that 1 should be considered to be the same as 2
(thus meaning that there is only one unique value and thus the maximum
cardinality restriction is not violated.

This is a particularly glaring example of the issue carefully chosen to use
built in terms for which we presume the unique names assumption holds and/or a
notion of inequality holds.

We might not want to ever choose option b above for built in terms from xml
for which we have a notion of uniqueness.

Even if we chose that method, we still have the problem of having a term that
is not a built in term from xml.
If for example, I say that I have a maximum cardinality of 1 on my has-pet
slot and then later find out that I have two fillers for my has-pet slot named
panda and monium,  if we attempt to do deductive closure, we should either
determine that I have at least 2 pets (thus creating a contradiction with the
maximum cardinality of 1) or we should assert that panda and monium refer to
the identical pet and thus I only have 1 pet.

Many systems have used the unique names assumption and thus chosen route a
above, thus I would have a contradiction on the number of pets and panda and
monium would not be considered to be one pet.

d
Dan Connolly wrote:

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

--
 Deborah L. McGuinness
 Knowledge Systems Laboratory
 Gates Computer Science Building, 2A Room 241
 Stanford University, Stanford, CA 94305-9020
 email: dlm@ksl.stanford.edu
 URL: http://ksl.stanford.edu/people/dlm/index.html
 (voice) 650 723 9770    (stanford fax) 650 725 5850   (computer fax)  801 705
0941

Received on Wednesday, 18 April 2001 22:04:36 UTC