Re: nominals and cardinalities

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