- From: Richard Fikes <fikes@KSL.Stanford.EDU>
- Date: Wed, 12 Sep 2001 22:16:07 -0700
- To: waldinger@AI.SRI.COM
- CC: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>
> 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