From: Pat Hayes <phayes@ai.uwf.edu>

Date: Thu, 13 Sep 2001 12:19:20 -0500

Message-Id: <p05101001b7c68674fe7c@[205.160.76.190]>

To: Richard Fikes <fikes@KSL.Stanford.EDU>

Cc: waldinger@AI.SRI.COM, "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>

Date: Thu, 13 Sep 2001 12:19:20 -0500

Message-Id: <p05101001b7c68674fe7c@[205.160.76.190]>

To: Richard Fikes <fikes@KSL.Stanford.EDU>

Cc: waldinger@AI.SRI.COM, "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. No, it is an issue. The axioms cannot *prevent* lists being infinite in length; but if lists are infinite, then the axioms don't do their intended job. So the axioms do not fully capture the intended meanings. >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)))) This seems to assume that (Integer ?n) is true of only finite objects, though, which begs the question. There is no way to axiomatize this in FOL which guarantees that all things satisfying this (or any other) predicate are finite in all models. For example, suppose that there are infinite lists, say with lengths w+1, w+2, etc., where w is the first transfinite ordinal, and also that w is an integer, ie (Integer ?n) is true when '?n' denotes w, w+1, etc.. Then both your axioms are satisfied, and any first-order version of the induction axiom for arithmetic can be be satisfied also. (This follows from the compactness theorem for FOL.) The only way to rule out models like this is to go beyond first-order logic, eg by using infinitary logic, as KIF does (implicitly) in the parts that you have decided, wisely, not to use in your axioms. Or, you could just say that your axioms aren't actually in FOL at all, but are in KIF, which is a subset of Lw1w. Then they would have content that wouldn't be fully captured by a first-order reasoner like SNARK, so you could just soar above the fray. We are doing semantics here, after all :-) Pat -- --------------------------------------------------------------------- IHMC (850)434 8903 home 40 South Alcaniz St. (850)202 4416 office Pensacola, FL 32501 (850)202 4440 fax phayes@ai.uwf.edu http://www.coginst.uwf.edu/~phayesReceived on Thursday, 13 September 2001 13:19:25 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:36 UTC
*