- From: Richard Fikes <fikes@KSL.Stanford.EDU>
- Date: Fri, 14 Sep 2001 10:54:06 -0700
- To: Richard Waldinger <waldinger@AI.SRI.COM>
- CC: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>, Pat Hayes <phayes@ai.uwf.edu>
> > 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.
Oh, I now see your point that the axioms for cardinality and
maxCardinality do not work if all lists are considered to be finite.
(The axiom for minCardinality doesn't appear to have the problem.)
However, that problem can apparently easily be fixed by requiring that a
NoRepeatsList of appropriate length exist rather than stating the
conditions in terms of all such NoRepeatsLists, as follows:
MAXCARDINALITY AXIOM
I had proposed the following axiom for maxCardinality:
%% 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 ?m)
(=> (and (NoRepeatsList ?vl ?m)
(forall (?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))
(=< ?m ?n))))))
{Note that in the above axiom I have made the correction regarding the
scoping of ?m that you pointed out in your message.}
That axiom says that object ?i is type ?r if and only if all
NoRepeatsLists containing exactly the values of property ?p at ?i have
length less than or equal to the maxCardinality ?n. We can change the
axiom to say that ?i is type ?r if and only if there exists such a
NoRepeatslist. I think that sidesteps the finiteness issue. The
revised axiom would be 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 "maxCardinality" for R, then an
object I is type R if and only if there exists a
"NoRepeatsLists" of length M such that the list's items are exactly the
values of P and 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)
(exists (?vl ?m)
(and (NoRepeatsList ?vl ?m)
(forall (?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v)))
(=< ?m ?n))))))
CARDINALITY AXIOM
I had proposed the following axiom for cardinality:
%% 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 there exists 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 ?m)
(=> (and (NoRepeatsList ?vl ?m)
(forall
(?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))
(= ?m ?n))))))
We can make an analogous change in this axiom as in the maxCardinality
axiom. Namely, require that there exist a NoRepeatsList of length ?n
containing exactly the values of ?p at ?i, 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 there exists a "NoRepeatsLists" of
length N whose items are exactly the values of P.
(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)
(exists (?vl)
(and (NoRepeatsList ?vl ?n)
(forall
(?v)
(<=> (PropertyValue
item ?vl ?v)
(PropertyValue
?p ?i ?v))))))))
---------------
> > 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).
Hmm. That is probably correct, and if so is simpler than what I
proposed. What we are both saying is needed (in the formulation that
uses lists) are axioms assuring that the needed NoRepeatsLists exist.
What we are both demonstrating is that adding such axioms can be done
without difficulty.
Richard
Received on Friday, 14 September 2001 13:54:14 UTC