W3C home > Mailing lists > Public > www-webont-wg@w3.org > May 2003

nominals and cardinalities

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
I've had a couple of ideas that I wanted to have recorded in the public

This is not intended to inform the discussion of CR/PR or responses to
Martin Merry.

Here's the simpler one.


"Combining Tableau and Algebraic Methods for Reasoning with
Quali?ed Number Restrictions in Description Logics"


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

In the initial ontology:
Replace every EnumeratedClass or oneOf construct by a union of singletons,

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.
   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

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

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

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