Re: class and inviduals

Hi all,
I am a bit lost in this longish discussion  for which I didn't yet
check the whole history and I am on holiday at the moment with very
limited internet access. It would be great if there was a more concise
problem description, then I'll get back to it at the end of next week.
Birte

On 20 November 2010 23:39, Bijan Parsia <bparsia@cs.man.ac.uk> wrote:
> On 20 Nov 2010, at 16:05, Pat Hayes wrote:
>
>> On Nov 20, 2010, at 6:47 AM, Bijan Parsia wrote:
> [snip]
>>> [snip]
>>>  once you have identity conditions in a given model other than extensional equivalence, then you typically (but not necessarily) have a first order theory. Both punning and F-Logic share this feature and it doesn't really matter whether you reflect this in the model theory or via translation into a fully sorted logic. (This is why the metaphysics is somewhat irrelevant.)
>>
>> Quite.
>
> I'm glad we all agree.
>
>>> Once you have this separation you can, in principle, have all sorts of ways of connecting statements about the "individual" and statements about the extension. For example, standard Hilog approaches (e.g., as described by Boris) differ from punning semantics by adding something like the following axiom schemata:
>>>      ?C = ?D => ?C equiv ?D.
>>
>> Yes. But note that if equality is understood in its 'normal' FO way, then this would be a tautology; which it is in CL.
>
> Well, sure, but that's just a matter of semantic presentation, not anything more interesting that that for our current discussion.
>
> Also, that's even only under certain conditions (once we've separated class identity from extensional equivalence). For example, consider a Henkin style semantics for punning wherein the extensional relation was parameterised with a name and it was not functional. Thus, a single individual could have multiple extensions *in the same model*. Now, individual identity wouldn't force extension identity. With such a model theory, you can get punning behavior *even with real identity* (and not just an equivalence relation).
>
> This is defensible on non-pragmatic grounds. Now, I certainly grant that it's not the most natural approach coming from a normal first to higher order perspective, but not all metamodelling is usefully modelled by successive approximations of second order logic. (Annotations come to mind.)
>
> Heck, it's even pretty reasonable to argue that with such a Henkin separation real identity is the wrong equivalence relation for "=". At the very least, you might want to make it impossible to make arbitrary class individuals possibly identical with arbitrary non class individuals.
>
> All this is just to say that we shouldn't give too much weight to certain consequences of certain semantic presentations esp. when we're going outside the bog standard situation (e.g., straight FOL; straight second order; etc.). There's just Too Much Choice for things to be dictated by logic alone.
>
> [snip]
>>> Now, I think punning as seen in OWL 2 DL has some problems for modellers. It was merely intended to bring OWL Full and OWL DL a bit closer together, not to solve metamodelling problems. In particular, I wanted it to cover the relative simple case where I've tried to integrate two ontologies with overlapping signatures where the overlap had conflicting sorts (i.e., the same term used as a class and as a property). Prior to OWL 2,if you had that, you were bumped out of OWL DL and the "right" behavior of tools was to give up (or push you to OWL Full). That was a loser, imho. The current situation is better.
>>
>> Agreed. Much better.
>
> The real question is where to go from there.
>
>>> I don't believe (and didn't during the OWL WG) that Hilog semantics was remotely worth the cost (undecidability or a Role UNA). What seems to be the most common case of Hilog like reasoning is in term mapping. There, I agree that if you are using "sameAs" to map synonymous terms, then you want C sameAs D to give you C equivalentTo D (where C and D are names). However, I really don't think you want a *reasoner* to do that work!
>>
>> If the reasoner is able to reason about equality - not an obvious choice, I would agree - then surely it should be able to do that work, as you put it.
>
> Yes, of course. But 1) it will also do more things and 2) it won't do that very well.
>
> Consider the following ontology under Hilog semantics:
>
>
>        bar type  (p max 2 Thing).
>        bar p C.
>        bar p D.
>        bar p E.
>
> Now, is C equivalentTo D? To E? To D or E?
>
> Well, let's consider the equality reasoning. Since bar can have at most 2 p successors, either C sameAs D, or D sameAs E, or C sameAs E.
>
> With hilog, thus, either C equiv D or D equiv E or C equiv E. (Non exclusive)
>
> This is nasty! It's a bit nasty computationally (more of a pita than a real problem), but I would argue that it's more nasty for typical modellers. It's hard to imagine (I failed) a case where this would make sense. It's even harder to imagine (for me) cases where this was a modelling boon.
>
> More typically, afaict, a modeller says "C sameAs D" where C and D are only used as classes (or the modeller doesn't know) as a cheap way of saying that these are synonymous terms. (Notice the "term" level speak, not object level!)
>
> Of course, in RDF(S) + sameAs, these cases coincide, so it's easy to use the "real" equality relation to do the term mapping. But that's misleading as you up the expressivity.
>
>> After all, the substitutivity of equals is pretty much the basic rule for equality reasoning.
>
> Meh. This is really a metaphysical argument. WRT counting, for example, punning behaves like "full" equality (C sameAs D, whether asserted or implies means that:
>        bar type (p max 1 Thing).
>        bar p C.
>        bar p D.
> is consistent.)
>
>> I'd go so far as to say that without that, you simply don't have equality in the language.
>
> Meh, again. First, I'd want to know, "So what?", more specifically, "What are the consequences and when do I have to keep in mind that I'm working with a non-equality equivalence relation" For OWL DL, the consequences basically are, "Don't use sameAs for term mapping" and when you need to keep it in mind is pretty much "When arguing with Pat".
>
> Hardly interesting, I'd say.
>
>> Better to accept that some reasoners are incomplete, in documented ways, than to warp the semantics so that the meaning of something this basic is altered, IMO.
>
> That's back to semantic presentation. If I use multiple extensions, then I can keep identity uniform.
>
> Oh. And who has a problem saying that OWL 2 DL is incomplete wrt Hilog semantics? No one. (At least not me.) It's also incomplete wrt other OWL Fullisms and it is a syntactic fragment of FOL.
>
> The real question is whether it ever makes sense to adopt Hilog semantics. I don't see a good case for the pain it'll bring. I suspect that other metamodelling semantics are more practically useful, as well.
>
> Note that I did make a good faith effort to investigate this during the OWL working group. It really isn't a high priority from a modelling perspective. I think we should embrace that face and manage term mapping (which *is* a high priority) in other ways.
>
>>> Such mapping are better treated as *mappings* and handled in a preprocessing stage (IOW, "sameAs" qua equality is the *wrong thing*). What full hilog semantics would give you over that is things like reasoning by cases where two terms are considered equal and then *not* equal.
>>
>> ? ? Can you elaborate on this a little, Bijan? Are you saying that hilog semantics would give you a nonmonotonic equality? (Surely not.)
>
> Nope.
>
>> Seems to me that equality in common logic, at any rate, is about a simple as equality can get.
>
> See my example above. OTOH, perhaps the Birte et al approach does this and does it at the cost of a linear number of additional axioms. It's not 100% clear to me (though I've not read the paper very carefully yet). This is possible as they don't apply Hilog semantics to roles. If so, then it's a lot cheaper (and easier to implement) than I had thought. Indeed, it could be implemented via preprocessing. Hmm.
>
> Ok, Table 3 sorta convinces me that that would work. If I make O_houseMouse same as O_fieldMouse,then...ok, no, I've lost it :) I see that you'd get the  MatSubClass axiom: Class      ⊓∀type− .∃type.{oC }≡Class⊓ ∃subClassOf.{oC} since those oCs are individuals. Equality there will substitute. But I don't see how we'd get back to C equiv D.
>
> Oops! Wait, Theorem 1 claim 1 rules it out, as all axioms in the signature of the original ontology entailed by the metamodelling  enabled ontology are entailed by the original ontology. Thus, we don't get from C=D to C equiv D.
>
> I've cced Birte to verify.
>
> Perhaps there's some clever way to reflect equalities without having to iterate to a fixed point and perhaps we can ignore disjunctive considerations. I don't know at this point :)
>
> A problem is that entailed equivalences can produce additional entailed equalities. So we can't, as in RDF(S), just do all the equality reasoning and then add all the equivalences. Consider:
>
>        C Equiv {E}.
>        D Equiv {F}.
>        E Equiv P some G.
>        F Equiv P only G.
>
> Now, let's make C = D. Without hilog, that's the only equality following from this ontology. But if we turn on hilog, then
>        C Equiv D.
> Which means:
>        {E} Equiv {F}.
> ({E} means oneOf(E), i.e., a nominal).
>
> But then
>        E = F!
> Which means
>        P some G equiv P only G.
>
> That's a bit surprising. And clearly the second equality required an iteration.
>
> That we hit a fixed point here and got all the entailments doesn't mean this is generally complete.
>
> Sorry to blather on so long. It's a complex topic even this tiny bit of it:(
>
> Cheers,
> Bijan.



-- 
Dr. Birte Glimm, Room 309
Computing Laboratory
Parks Road
Oxford
OX1 3QD
United Kingdom
+44 (0)1865 283520

Received on Sunday, 21 November 2010 09:50:25 UTC