W3C home > Mailing lists > Public > public-owl-dev@w3.org > October to December 2010

Re: class and inviduals

From: Pat Hayes <phayes@ihmc.us>
Date: Sat, 20 Nov 2010 10:05:23 -0600
Message-Id: <BEB50E25-CAF6-4F60-B98B-F1882C924ABF@ihmc.us>
Cc: Enrico Franconi <franconi@inf.unibz.it>, public-owl-dev@w3.org
To: Bijan Parsia <bparsia@cs.man.ac.uk>

On Nov 20, 2010, at 6:47 AM, Bijan Parsia wrote:

> Really not wanting to get caught up in the silly parts, but...
> 
> (and yes, that disclaimer is *more* likely to enmesh me. Oh well.)
> 
> On 19 Nov 2010, at 10:24, Enrico Franconi wrote:
> [snip]
> 
>> If you want a logic-based language where class and individual names blur, there are three semantic choices which I am listing from the weakest to the strongest (note: a stronger logic is the one which is able to restrict more the models and therefore it gives more inferences; in this case, all inferences of a weaker logic are also inferences of the stronger logic):
>> 1) Contextual FOL (aka punning): adopted by OWL-DL;
>> 2) F-Logic semantics: adopted by RDF(S) and common logic;
>> 3) high-order logic.
> 
> [snip]
> 
> For the interesting reading, let me point out that this is a bit of a simplification (deliberately so, on Enrico's part). If we are just considering things from the logic perspective (that is, abstract from at least metaphysics and perhaps usability), once you separate the "existence" of a class from its extension, that is, 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. 

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

> where ?C and ?D get bound to *names*. Notice, of course, that one could write all sorts of axiom schemata,
> 	foaf:knowsaswellasitself(?C, ?D) => ?C subClassOf ?D.
> 
> (All this could equally well be specified model theoretically.)
> 
> You could introduce other conditions (e.g., stratification), as well. They may or may not be useful, usable, computable, etc. For a nice example, see Birte Glimm et al's paper at this ISWC:
> 	http://www.comlab.ox.ac.uk/files/3318/TR-GRV-Metamodelling.pdf
> 
> 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.
> 
> 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. After all, the substitutivity of equals is pretty much the basic rule for equality reasoning. I'd go so far as to say that without that, you simply don't have equality in the language. 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.

> 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.) Seems to me that equality in common logic, at any rate, is about a simple as equality can get. 

Pat

> I was not able to elicit from anyone a situation where this would be *intelligible* much less helpful. I remain open to seeing some case studies.
> 
> Cheers,
> Bijan.
> 
> Cheers,
> Bijan.
> 

------------------------------------------------------------
IHMC                                     (850)434 8903 or (650)494 3973   
40 South Alcaniz St.           (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (850)291 0667   mobile
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes
Received on Saturday, 20 November 2010 16:06:25 GMT

This archive was generated by hypermail 2.3.1 : Wednesday, 27 March 2013 09:32:58 GMT