- From: Enrico Franconi <franconi@inf.unibz.it>
- Date: Sat, 20 Nov 2010 13:58:25 +0100
- To: Bijan Parsia <bparsia@cs.man.ac.uk>
- Cc: public-owl-dev@w3.org
It happens that I agree with both parts of Bijan's analysis at 100%! --e. On 20 Nov 2010, at 13:47, 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.) 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. > 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. > > 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! 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. 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.
Received on Saturday, 20 November 2010 12:59:12 UTC