- From: Richard Waldinger <waldinger@AI.SRI.COM>
- Date: Thu, 13 Sep 2001 18:33:28 -0700
- To: Richard Fikes <fikes@KSL.Stanford.EDU>
- CC: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>, Pat Hayes <phayes@ai.uwf.edu>
Richard Fikes wrote----
>
> 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.
>
Right, the axioms straddle the fence on the finite-ness issue. But to
prove the desired properties of carinality restrictions, we need to add
an axiom that will, under ordinary models, force some lists, or sets, to
be infinite.
>
> 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.
What you need is to add an axiom that ensures the existence of the
finite *or infinite* NoRepeatsList, or set, that contains the set of all
values of a given property.
> However, I think there is a much simpler
> fix than introducing a set theory.
Introducing infinite lists seems more disturbing to me than introducing
infinite sets. People are used to lists being finite. Also, I only
needed to add a few axioms. But infinite lists work work too.
> 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.
> 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]
This says that ?l is a NoRepeatsList of length ?n.
Fine, but you could just as well have left the definition the same and
said
(and (NoRepeatsList ?l)(length ?l) = ?n)
>
> 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))))
You shouldn't need an axiom for this. Just take
?l2 to be Cons(?x, ?l1).
So adding this "axiom" doesn't change the theory.
>
> 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 "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))))))
First of all, ?m has no quantifier. You probably don't mean it to be
universally quantified over the whole axiom, which is the default, so
i'll assume that you really meant
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue cardinality ?r ?n))
(forall (?i)
(<=> (Type ?i ?r)
(forall (?vl ?m)
(=> (and (NoRepeatsList ?vl ?m)
(forall (?v)
(<=> (PropertyValue item ?vl ?v)
(PropertyValue ?p ?i ?v))))
(= ?m ?n))))))
It looks as if this will have the same problem as the original axiom.
Consider a model in which all lists are finite, ?p is hasFather, and ?n
is 1.
Say were are trying to define a restriction ?r =
OneFatherClass, the class of all elements that have precisely one
father. Suppose that we are on a planet in which i0 is a creature who
has an infinite number of fathers. There is no NoRepeatsList ?v1 of any
finite length ?m that contains precisely the fathers of i0, because i0
has infinitely many fathers. Hence, vacuously, all such lists have
length 1. That is, i0 is indeed a member of OneFatherClass. But,
contrary to our expectation, i0 does not have precisely one father.
The finiteness issue might be a red herring here. The point is that
there is no axiom that ensures that there exists a NoRepeatsList
containing precisely the elements who have one father.
I realize that I am putting words into your mouth by my placement of the
quantifier for ?m, but I don't see any way of getting around the
problem, wherever we put the quantifier.
----Richard W.
_________________________________
Richard Fikes wrote:
>
> > 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 21:34:35 UTC