Re: Infinite cardinalities

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

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

> Ken may have pointed out a problem with the KIF axiomatization for
> DAML+OIL.  
> 
> However, even if we make the condition that properties have some local
> finiteness built into them (and I'm not even sure if this does follow from
> the KIF axiomatization, and it is certainly not in the model-theoretic
> semantics), this does not mean that the entire domain is finite, nor does
> it mean that a property (taken as a whole) need have a finite extension.
> 
> peter
> 
> 
> 
> 
> From: Ken Baclawski <kenb@ccs.neu.edu>
> Subject: Infinite cardinalities
> Date: Sun, 1 Apr 2001 17:34:48 -0400 (EDT)
> 
> > Recently, Peter Patel-Schneider mentioned that DAML+OIL allows infinite
> > models.
> > 
> > On Fri, 30 Mar 2001, Peter F. Patel-Schneider wrote:
> > 
> > > ...
> > > DAML+OIL does not have a finite model restriction.  It is entirely possible
> > > to have DAML+OIL models with an infinite number of objects that are not
> > > datatype values.
> > > ...
> > 
> > Furthermore, the preface to the DAML+OIL axioms makes this statement which
> > seems to allow for models that have infinite cardinalities:
> > 
> > "This axiomatization is designed to place minimal constraints on the
> > interpretation of the non-logical symbols in the resulting logical theory. 
> > In particular, the axioms do not require use of a set theory, that classes
> > be considered to be sets or to be unary relations, nor do they require
> > that properties be considered to be mappings or binary relations." 
> > 
> > However, the axioms make frequent use of finite lists, which are much more
> > restrictive than sets.  Because of this there are implicit finiteness
> > assumptions in the axioms.  Consider for example Axiom 105: 
> > 
> > Ax105.(=> (and (PropertyValue onProperty ?r ?p)
> >                      (PropertyValue minCardinality ?r ?n))
> >                 (forall (?i) 
> >                         (<=> (Type ?i ?r) 
> >                              (exists (?vl) 
> >                                      (and (no-repeats-list ?vl) 
> >                                           (forall (?v) 
> >                                                   (=> (PropertyValue 
> >                                                         item ?vl ?v) 
> >                                                       (PropertyValue
> >                                                         ?p ?i ?v))) 
> >                                           (>= (length ?vl) ?n))))))[9]
> > 
> > It follows from this axiom that restricting a property to have
> > minCardinality of 0 has the side-effect of restricting the cardinality to
> > be finite.  Is this what was intended?  Does DAML+OIL really support
> > infinite cardinalities?
> >
> > Ken Baclawski
> > College of Computer Science
> > Northeastern University
> > kenb@ccs.neu.edu
> > 
> > 
>

Received on Monday, 2 April 2001 09:01:49 UTC