From: Ian Horrocks (horrocks@cs.man.ac.uk)
Date: 02/06/01
On February 5, pat hayes writes: > After thinking about this issue longer and (in particular) trying to > come up with a killer example, I have to agree that there isn't one. > Or at any rate not one I can think of, that couldnt be done with > disjoint concrete domains with only a slight artificiality, at worst. > So, and given Deborah's eloquent testimonial, I withdraw my > objections and apologise for (being a contributory factor towards) > causing so much trouble. > > I still don't follow what the technical reasons for the need for > this, er, classical split actually are, though, and would appreciate > any pointers to where they are discussed in the literature. Pat, For the language we have, the split may not be "necessary", but it is very convenient (from a practical viewpoint) and, as Deborah and now you have pointed out, it is hard to think of examples where the separation is a serious inconvenience. If we extend the language to include comparisons (e.g., salary > age), then the separation is necessary in order to maintain decidability (see [1]). More generally, work by Baader and Wolter on combining (modal) logical languages (see [2] and [3]) shows that in general using this kind of separation trick results in a "fusion" that inherits many of the properties of the separate languages and which allows for the design of "hybrid" reasoning systems for the new language (i.e., by combining reasoners for the two original languages). In contrast, a simple union of two logical languages almost always leads to a complexity explosion and requires the design of completely new reasoning procedures: see the work of Marx [4] for example. Going back to the practical argument, the "split" allows us to take any system of datatypes for which we can build a checker/validator (i.e., a decision procedure for the emptiness of an expression of the form D1 ^ ... ^ D n , where di is a (possibly negated) concrete datatype) and form a "fusion" with daml+oil. The fusion will be decidable and we can build a "hybrid" decision procedure for it via a relatively simple combination of a daml+oil decision procedure and the datatype checker/validator. An unrestricted combination does not have these nice properties: the decidability of the language is not determined by the decidability of the two components, and we can't take advantage of the hybrid reasoning technique because of the interaction between the domains. Consider, for example, a class with a property P1 whose value is (C AND (integer 1)) and a property P2 whose value is ((not C) AND (integer >0) AND (integer <2)). A hybrid reasoner wont be able to tell that this class is inconsistent (because the value of both P1 and P2 must have the same interpretation). Regards, Ian [1] Baader, F. and Hanschke, P., Extensions of Concept Languages for a Mechanical Engineering Application, Proceedings of the 16th German AI-Conference (GWAI-92), 1993, pp132--143, Springer--Verlag. [2] http://www.informatik.uni-leipzig.de/~wolter/ [3] http://www-lti.informatik.rwth-aachen.de/ti/baader-en.html [4] http://turing.wins.uva.nl/~marx/papers.html
This archive was generated by hypermail 2.1.4 : 04/02/02 EST