- From: Jeremy Carroll <jjc@hplb.hpl.hp.com>
- Date: Tue, 13 May 2003 17:53:59 +0200
- To: <www-webont-wg@w3.org>

I have been thinking about how one might implement nominals more effectively. I've had a couple of ideas that I wanted to have recorded in the public list. This is not intended to inform the discussion of CR/PR or responses to Martin Merry. Here's the simpler one. In http://kogs-www.informatik.uni-hamburg.de/~haarslev/publications/m4m2.pdf "Combining Tableau and Algebraic Methods for Reasoning with Quali?ed Number Restrictions in Description Logics" by Volker Haarslev, Martina Timmann, Ralf Möller we read how to combine a tableau reasoner with a solver for integer linear programs (systems of linear inequalities with integer solutions). They address the problems associated with qualified cardinality constraints. These techniques can be extended to address problems associated with cardinalities of finite and infinite classes by the following steps. We augment the solver of systems of linear inequations to support infinity as a possible number, i.e. variables range over the nonNegativeIntegers and infinity. In the initial ontology: Replace every EnumeratedClass or oneOf construct by a union of singletons, e.g. oneOf( a b c ) is replaced by unionOf( oneOf(a) oneOf(b) oneOf(c) ) Any particular tableau can then be annotated with a set of linear inequations linking the cardinalities of classes and properties. e.g. a subClassOf b ==> Card(a) <= Card(b) c = unionOf(a b) && DisjointClasses(a b) ==> Card(c) = Card(a) + Card(b) oneOf(a) ==> Card(oneOf(a)) = 1 EquivalentClasses( a b ) ==> Card(a) = Card(b) Card(Restriction( p cardinality=N )) <= Card(p)/N If the annotations on a tableau are an insoluble system of linear inequations then the tableau was inconsistent. Otherwise a solution to the system of linear inequations can be converted into an instance of the ontology for a completed tableau by simply instantiating each class and property with the given cardinality. (the instantiation step can be omitted, and must be omitted for infinite classes!) It may be necessary to improve the treatment of oneOf(a b c) with the rules Card(oneOf(a b c)) <= 3 and Card(oneOf(a b c))>= 1 as opposed to the rather conservative initial step of splitting it into a union of singletons. Integration between these inequations and any knowledge of the distinctness or identity of the names a, b and c is desired. More generally, as in Haarslev et al's paper it is advantageous to divide the classes up into disjoint subclasses, so that unionOf's can be replaced by disjointUnionOf's and hence inequations can be replaced by equations. The example given with a cardinality restriction is some what simplistic: we need to ensure that all the inequations connected with such restricitions are satisfied: More examples Card(p) = Card(inverseOf(p)) Card(Restriction( p maxCardinality=N+1)) = Card(Restriction( p cardinality=N+1 ) ) + Card(Restriction( p maxCardinality=N)) Card(Restriction( p minCardinality=N)) <= Card(p)/N Jeremy

Received on Tuesday, 13 May 2003 11:55:15 UTC