From: pat hayes <phayes@ai.uwf.edu>

Date: Thu, 19 Apr 2001 23:58:20 -0500

Message-Id: <v04210119b7056e09b002@[205.160.76.206]>

To: Dan Connolly <connolly@w3.org>

Cc: Richard Fikes <fikes@KSL.Stanford.EDU>, www-rdf-logic@w3.org

Date: Thu, 19 Apr 2001 23:58:20 -0500

Message-Id: <v04210119b7056e09b002@[205.160.76.206]>

To: Dan Connolly <connolly@w3.org>

Cc: Richard Fikes <fikes@KSL.Stanford.EDU>, www-rdf-logic@w3.org

>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/~phayesReceived on Friday, 20 April 2001 00:58:36 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:38:20 UTC
*