- 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