Re: Infinite cardinalities

On Mon, 2 Apr 2001, Peter F. Patel-Schneider wrote:

> From: Ken Baclawski <kenb@ccs.neu.edu>
> Subject: Re: Infinite cardinalities
> Date: Mon, 2 Apr 2001 09:01:45 -0400 (EDT)
> 
> > I did not mean to suggest that this was more than a local condition.  And,
> > in fact, axiom 105 is okay.  It only assumes that the list is a subset of
> > the set of values.  However, lists are used in a few other places as well. 
> > They are used to define containers (Axiom 13), to define unionOf,
> > disjointUnionOf, intersectionOf, etc.  There is still the question of
> > whether DAML+OIL should support (local) infinite cardinalities.
> >
> > The use of list for Axiom 13 is particularly noteworthy.  Axiom 66 states
> > that lists are sequences, Axiom 14 implies that sequences are containers
> > and Axiom 13 states that containers are lists.  It appears to be a cycle.
> > It is not an actual cycle because Axiom 13 is using the built-in
> > KIF list, not the DAML list, but it isn't clear that it is entirely
> > consistent either.
> > 
> > Ken Baclawski
> > College of Computer Science
> > Northeastern University
> 
> The ...Of lists are part of the syntax of the language, which is indeed
> finite, and finite by design, so this is OK.   The other concerns above
> should be investigated by the authors of the axiomatization.

Perhaps it is too late to change this, but here is a design for the
unionOf construct that is not restricted to finite (or even countable)
unions:

(=> (and (PropertyValue value ?r unionOf)
         (PropertyValue onProperty ?r ?p))
    (and (forall (?c) (=> (PropertyValue ?p unionOf ?c)
                          (Type ?c Class)))
         (forall (?x) (<=> (Type ?x ?r)
                           (exists (?c) (and (PropertyValue ?p unionOf ?c)
                                             (Type ?x ?c)))))))

The other ...Of constructs could be handled similarly.  This construct
is in the spirit of the other uses of Restriction classes.  It defines the
restriction class to have instances that are exactly the instances in the
union of the classes that are linked to the unionOf resource by the
property ?p.

No doubt one could come up with even better designs than this one, but it
shows that it could be done.

Ken Baclawski
College of Computer Science
Northeastern University

Received on Monday, 2 April 2001 22:42:00 UTC