Re: Revised Axioms for Cardinality Restrictions

> In an earlier message I mentioned a weakness in the axioms for some of
> the DAML cardinality restrictions, in
>  http://www.daml.org/2001/03/axiomatic-semantics-071601.html , 
> that made it impossible to prove some expected properties

> The axiom in the current axiomatic semantics document that defines
> cardinality restrictions is, in KIF notation,
> 
> (=> (and (PropertyValue onProperty ?r ?p)          [cardinality axiom 3]
>          (PropertyValue cardinality ?r ?n))
>     (forall (?i)
>        (<=> (Type ?i ?r)
>             (forall (?vl)
>               (=> (and (NoRepeatsList ?vl)
>                        (forall (?v)
>                          (<=> (PropertyValue item ?vl ?v)
>                               (PropertyValue ?p ?i ?v))))
>                   (= (length ?vl) ?n))))))
> 
> In other words, if r is a cardinality restriction with onProperty p and
> cardinality component n, then an element i is of type r if and only if,
> for any nonrepeating list v1 that contains precisely the elements v
> such that p(i, v), the length of v1 is n. The axiom makes use of the
> DAML convention that
>   PropertyValue(p, i, v)
> means p(i, v). 
> 
> The problem is that there is nothing in the axioms that implies the
> existence of such a list v1.   In particular, the axioms are agnostic
> about whether lists are finite or infinite.  A possible model of the
> DAML axioms is one in which all lists are finite.

As discussed earlier, the cardinality axioms that use NoRepeatsList do
not require or assume that lists can be infinite in length.  So, that is
not an issue.

I agree with your observation that the cardinality axioms are flawed in
that there is nothing in the axioms that entails the existence of a
NoRepeatsList containing any given finite set of values of a given
property for a given object.  However, I think there is a much simpler
fix than introducing a set theory.  That is, I think we can modify the
axioms so that the existence of a NoRepeatsList containing any given
finite number of objects is assured.  Attached below is a
straightforward way of doing that.

Comments welcome.

Richard

--------------------------
Add a second argument to relation NoRepeatsList that is the length of
the list.  Then, the axiom defining NoRepeatsList becomes the following:

(<=> (NoRepeatsList ?l ?n)
     (or (and (= ?n 0) (= ?l nil)) 
         (and (= ?n 1) (exists (?x) (= ?l (listof ?x)))) 
         (and (not (item (rest ?l) (first ?l))) 
              (NoRepeatsList (rest ?l) (- ?n 1)))))  	[NoRepeatsList
axiom 1]

Add an axiom stating that NoRepeatsLists exist for any finite collection
of objects as follows:

(=> (and (Integer ?n)
         (>= ?n 0)
         (NoRepeatsList ?l1 ?n) 
         (not (item ?l1 ?x)))
    (exists (?l2) (and (NoRepeatsList ?l2 (+ ?n 1)) (item ?l2 ?x))))

Modify the axioms for minCardinality, cardinality, and maxCardinality in
the obvious way as follows:

%% If a property P is a value of "onProperty" for a restriction R and a
non-negative integer N is a value of "minCardinality" for R, then an
object I is type R if and only if there is a "NoRepeatsList" of length M
such that all of the list's items are values of P for I and M is greater
than or equal to N.  (I.e., a "minCardinality" restriction of N on a
property P is the class of all objects I which have at least N values of
P.)
(=> (and (PropertyValue onProperty ?r ?p)
         (PropertyValue minCardinality ?r ?n))
    (forall (?i) 
            (<=> (Type ?i ?r) 
                 (exists (?vl ?m) 
                         (and (NoRepeatsList ?vl ?m) 
                              (forall (?v) 
                                (=> (PropertyValue item ?vl ?v) 
                                    (PropertyValue ?p ?i ?v))) 
                              (>= ?m ?n))))))

%% If a property P is a value of "onProperty" for a restriction R and a
non-negative integer N is a value of "maxCardinality" for R, then an
object I is type R if and only if for all V1, if V1 is a
"NoRepeatsLists" of length M such that the list's items are exactly the
values of P, then M is less than or equal to N.  (I.e., a
"maxCardinality" restriction of N on a property P is the class of all
objects I which have at most N values of P.)

(=> (and (PropertyValue onProperty ?r ?p)
         (PropertyValue maxCardinality ?r ?n))
    (forall (?i) 
            (<=> (Type ?i ?r)
                 (forall (?vl) 
                         (=> (and (NoRepeatsList ?vl ?m) 
                                  (forall (?v) 
                                          (<=> (PropertyValue 
                                                 item ?vl ?v) 
                                               (PropertyValue 
                                                 ?p ?i ?v))))
                             (=< ?m ?n))))))

%% If a property P is a value of "onProperty" for a restriction R and a
non-negative integer N is a value of "cardinality" for R, then an object
I is type R if and only if for all V1, if V1 is a "NoRepeatsLists" of
length M whose items are exactly the values of P, then M is equal to N. 
(I.e., a "cardinality" restriction of N on a property P is the class of
all objects I which have exactly N values of P.)

(=> (and (PropertyValue onProperty ?r ?p)
         (PropertyValue cardinality ?r ?n))
    (forall (?i) (<=> (Type ?i ?r)
                      (forall (?vl) 
                              (=> (and (NoRepeatsList ?vl ?m) 
                                       (forall 
                                         (?v) 
                                         (<=> (PropertyValue 
                                                item ?vl ?v) 
                                              (PropertyValue 
                                                ?p ?i ?v))))
                                  (= ?m ?n))))))

Received on Thursday, 13 September 2001 01:16:14 UTC