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

Date: Tue, 24 Sep 2002 13:59:43 -0500

Message-Id: <p05111b55b9b6408c0349@[65.217.30.172]>

To: Ian Horrocks <horrocks@cs.man.ac.uk>

Cc: www-webont-wg@w3.org

Date: Tue, 24 Sep 2002 13:59:43 -0500

Message-Id: <p05111b55b9b6408c0349@[65.217.30.172]>

To: Ian Horrocks <horrocks@cs.man.ac.uk>

Cc: www-webont-wg@w3.org

>On September 17, pat hayes writes: > >[snip] > >> >Finally, I would like to point out (again) that DLs are nothing more >> >than decidable subsets of FOL with useful computational >> >properties. >> >> You keep saying this, but that isn't the impression I get. For >> example, the recent DQL document has to have a footnote pointing out >> that DAML doesn't have any notion of 'conjunction', strictly >> speaking. > >It doesn't say that, it says that "DAML+OIL does not have a logical >connective for conjoining sentences or for conjoining knowledge >bases". It is simply the case that in DAML+OIL the use of the >conjunctive connective is not defined for sentences or KBs (it would >be easy to add such a definition). The lack of such a definition >doesn't stop the language from being (isomorphic with) a SUBSET of >FOL. Without conjunction, it must be a pretty trivial subset. That rules out all the binary connectives. > >> So the inference >> >> A, B |= (A and B) >> >> which is about the simplest inference imaginable, so simple that >> Aristotle didn't bother to give it a name, apparently isn't supported >> by DLs. > >In a DL there are some syntactic restrictions on the form of A and B: >recall that it is a SUBSET of FOL and not full FOL. If A and B are >classes (i.e., formulae with one free variable), then there is no >problem: > >A(x),B(x) |= (A and B)(x) > >for all A, B and x. ?? That isn't a valid FOL inference. Its not even *well-formed* in FOL. The nearest FOL expression that I can think of (and its only FO if you allow a free-wheeling KIF style of syntax) is: A(x), B(x) |= (exists (C) (forall (y) (iff C(y) (and A(y) B(y) )))), C(x) which is also not FOL valid, but it might be a reasonable axiom in a simple theory of predicates/sets. > >> And the 'strong' OWL semantics requires us to assert (or >> assume) that the class (union A B) must *exist* in order to validate >> the DL version of the inference >> >> A |= (A or B). > >again, it does: > >A(x) |= (A or B)(x) That is not the inference I cited. The difference is instructive, in fact: I cited an elementary principle of propositional reasoning, one that is incorporated into all human languages and probably into most human thought processes; and in return you cited a special case of a set-theoretic comprehension axiom which is not first-order valid. > >> That sure doesn't feel like a subset of FOL to me; it feels a lot >> more like a subset of ZF set theory. Those inferences are valid in >> propositional logic where there aren't any classes to exist in the >> first place. Union and intersection are *analogous* to disjunction >> and conjunction, but they are not the *same*. > >This is getting silly. I don't agree, I think it is central. >The correspondence between Description/modal >logics and *standard* FOL is very well know, e.g., see [1] for an >overview and relevant results dating back to the 1960s. I know about the *correspondence*. >I don't want >to get into a philosophical argument about what it means to be the >"same". For me it is enough to point out that DLs and their >corresponding fragment of FOL have models that are completely >isomorphic. Well, sorry, but this 'philosophical argument' (interesting that you use 'philosophical' as a dismissive; its a revealing rhetorical device often used by engineers) is central to what we are trying to do here. Its not just about isomorphic models. At the very least, we should be paying some closer attention to proof theory; but more centrally, the ways of thinking embodied in these logical frameworks need to be taken seriously. The entire game is to develop a 'web logic' that will enable people to mark up their websites with intuitively reasonable information expressed in a machine-useable form. These people are not going to have read [1] and are not going to find it natural to be forced to fit their thinking into a straightjacketed form, even if it is mathematically isomorphic to a more natural one; particularly if that form requires them to adopt a 'philosophical' (it would be more accurate to say 'ontological') framework for thinking that runs counter to the one they actually think with. For example, the idea that one should only be allowed to conclude A and B from B and A under restricted circumstances, and that this can only be done by concluding that new predicates exist is, frankly, ridiculous. The DL framework forces us all - lay users and us techies - into thinking about the existence of classes all the time. And that is not a natural way to think, for many purposes. (For some, but not for all.) Just look, for example, at the extraordinary lengths that Peter and I have been driven by the need to justify these silly 'closure' conditions on the OWL universe. I say silly because if the actual logical content of OWL were all written out straightforwardly in sentential form, the existence of the relevant domains would be a trivial consequence of Herbrand's theorem; the issue would not even arise. And yet, not only does it arise, purely as an artifact of the warped semantic framework of DLs, but it is seen as central, a stumbling block to progress and a huge obstacle to comprehension by implementers and users. It is a very bad sign, for example, that Russell's paradox even became a topic of conversation in Webont, let alone a topic that has diverted our best efforts for over 9 months. The logicians had that one settled in about 1930, before Tarsky even invented model theory. It just should never have come up. It only did because some people apparently think that saying (A and B) involves creating a class (lambda x. (A and B)(x) ). You are always emphasizing the fact that we cannot afford to indulge in original research work: we must stick to the standards. But when it comes to the basic framework of the languages, the standard were worked out over 50 years ago, and yet you insist on rejecting this well-understood framework and dragging us into this swamp of closure conditions, comprehension principles, recursive domains and fussy limitations on expressivity. Sorry, Ian, but you are wrong. DL's may be *isomorphic* to a subset of FOL, via a curious mapping (Im not even fully persuaded of this, by the way: are DL's always compact, for example? They refer to integers in their semantic conditions, which is slightly worrying) but they are definitely not a subset of FOL; and their syntax , metatheory and semantics are all quite unlike FOL. Most of OWL is not even FOL logically valid. FOL semantics does not support any inference to the existence of an un-named predicate. >I must say that I just don't understand what your problem is with >this. My problem, which has been present since I first got involved with DAML but which I have largely kept quiet about in the interests of making progress, not rocking the boat, etc.., is that the entire SW effort is being driven along a path which I am increasingly convinced is the wrong path for it to be on. It has been hijacked by the description logicians, and the anti-logic fuzzies have let this happen because both of them can agree over a drink that, whatever else may separate them, neither of them would ever want Webont to be an actual *logic*. (Heavens to Betsy, what a terrible idea!) And the result has been that Webont is now in a blind alley, trying to persuade the entire planet to adopt a notation which is at odds with about a century of clear understanding of meanings, proofs and connections to thought and language, all of which has been tossed aside. And as a result we are trapped in all kinds of arcane technical debates which are completely irrelevant to almost everyone, and tiptoeing nervously around issues which we should be able to settle in an afternoon and implement in a couple of weeks ( like how to incorporate "rules", by which people mean simple implications. Use Horn clauses, do backtracking with an efficient unification algorithm, OK? End of story, for God's sake. Stefan implemented it already months ago. Lets get on with something more interesting and useful.) My experience with trying to make sense of OWL has left me with the overwhelming feeling that this whole DL framework has now become more of a burden than it is worth. And it is, to make the point once more, NOT a subset of FOL. That claim is literally false and (IMO) highly misleading. It is a subset of a first-order set theory; and it is centrally concerned, like all set theories, with the complex and subtle ways in which its comprehension principles interact, and the need to provide just enough sets but not too many. This is a fascinating topic in foundations of mathematics, but (1) we are all of us amateurs at it, and (2) it seems totally irrelevant to the SW. We would be better spending our time helping Tim get N3 sorted out. Pat -- --------------------------------------------------------------------- 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 Tuesday, 24 September 2002 14:59:35 UTC

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