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

Date: Thu, 15 May 2003 19:10:20 +0100

Message-ID: <16067.55308.833734.647949@galahad.cs.man.ac.uk>

To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>

CC: www-webont-wg@w3.org

Date: Thu, 15 May 2003 19:10:20 +0100

Message-ID: <16067.55308.833734.647949@galahad.cs.man.ac.uk>

To: "Jeremy Carroll" <jjc@hplb.hpl.hp.com>

CC: www-webont-wg@w3.org

On May 13, Jeremy Carroll writes: > > > 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. Jeremy, The case of cardinality constraints and nominals really isn't comparable. Reasoning with cardinality constraints can be localised to a node (in a tableaux) and its immediate neighbours. Ensuring/proving that this is the case accounts for a lot of the tricky stuff in tableaux algorithms/proofs (e.g., it is the reason for the constraint on using transitive properties in cardinality restrictions). Reasoning with nominals, on the other hand, is global, which complicates matters enormously (as you obviously recognise to some extent). In particular, nominals mean that we can no longer explore only tree-like models, but have to consider arbitrary models. This makes it MUCH more difficult to ensure termination. > If the annotations on a tableau are an insoluble system of linear > inequations then the tableau was inconsistent. This is completely false. What it means is that some nodes may need to be identified. You would need to check the consistency of all possible combinations. The result of the combinations is non-tree models. The result of that is that we don't know how to catch cycles and ensure termination. Ian > 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 Thursday, 15 May 2003 13:59:29 UTC

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