nominals and cardinalities

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