Re: Cardinality Restriction Axioms too Weak

Richard: your point seems to depend on the claim that all lists are 
finite. Where do you derive that claim from? If we allow infinite 
lists into the universe then the cardinality axioms stated in terms 
of lists being of length one would seem to work (?). (Provided of 
course that we have the concept of 'one' available.)

But we have to allow infinite lists into the universe, since there is 
no way to characterize (axiomatise) the concept of 'finite' in any 
first-order subset of KIF.  The KIF notion of 'list' is defined in 
the KIF 3.0 documentation using sequence quantifiers, which are not 
first-order. The 'axiomatic semantics' however is restricted to the 
first-order sublanguage of KIF, so cannot impose the finiteness 
condition on the universe of lists. We can define 'list' so as to 
mean 'finite list', but only in a subset of KIF that is 
equiexpressive with an infinitary subset of Lw1w, not in the 
first-order fragment; and in that infinitary language, the required 
restriction on cardinality *can* be stated since we can define 
'finite integer' in that language. So either way, the cardinality 
restrictions seem to work.

(What wouldn't work however is any axioms that depend on a 
'recursion' applied to lists always terminating.)

Does Specware make some implicit assumptions about finiteness that 
may not be exactly appropriate here?

Pat Hayes


>I know there has been a lot of discussion about restrictions, but I
>think this is a different wrinkle.  This has to do with several
>varieties of cardinality restrictions.  It appears as if these axioms
>are not strong enough to prove simple consequences that anyone would
>expect to be true.  These problems were found in attempting to use
>Kestrel's Specware System, and the embedded SRI theorem prover SNARK,
>to verify some of these consequences.
>
>For example, in the DAML Language Walkthrough
>  http://www.daml.org/2001/03/daml+oil-walkthru.html
>the class Person is defined in part as a class of objects having
>precisely one father:
>
>  <rdfs:subClassOf>
>    <daml:Restriction daml:cardinality="1">
>      <daml:onProperty rdf:resource="#hasFather"/>
>    </daml:Restriction>
>  </rdfs:subClassOf>
>
>One would expect that it would follow from this that each person has
>precisely one father.  In fact, from the axioms in the Axiomatic
>Semantics document,
>  http://www.daml.org/2001/03/axiomatic-semantics-071601.html
>it does follow that each person has at least one father, but not, it
>seems, that a person cannot have two fathers.
>
>The above restriction can be expressed in axioms (in Specware notation)
>as
>
> axiom person-in-fatherclass is
>  PropertyValue(subClassOf, Person, FatherClass)
>
>[Every Person is in the FatherClass, where FatherClass is the anonymous
>restriction, of objects with precisely one father.]
>
>
> axiom onproperty-of-fatherclass-is-hasfather is
>  PropertyValue(onProperty, FatherClass, hasFather)
>
>[The onProperty of FatherClass is hasFather.]
>
>
> axiom cardinality-of-fatherclass-is-one is
>  PropertyValue(cardinality, FatherClass, 1)
>
>[The cardinality of FatherClass is 1.]
>
>Note that the names attached to axioms are only for our
>convenience--they have no logical significance.
>
>
> From this and the axioms for restrictions we would expect to be able to
>prove the following conjecture:
>
> conjecture people-have-at-most-one-father is
>  fa(i : Element, p1 : Element, p2 : Element)
>   Type(c, Person) &
>   PropertyValue(hasFather, i, p1) &
>   PropertyValue(hasFather, i, p2) =>
>   p1 = p2
>
>In other words, if a person i has two fathers p1 and p2, then p1 and p2
>must be the same.
>
>By properties of lists, to show that p1 and p2 are the same, it suffices
>to show that they are both items on a list of length 1. One way to do
>this is to appeal to the definition of cardinality,
>
> axiom definition-of-cardinality is
>  fa(r : Element, p : Element, n : Nat)
>   ((PropertyValue(onProperty, r, p) &
>     PropertyValue(cardinality, r, n)) =>
>    (fa(i : Element)
>     (Type(i, r) <=>
>      (fa(l : Element)
>       ((NoRepeatsList(l) &
>         (fa(v : Element)
>           (Item(l, v) <=>
>            PropertyValue(p, i, v)))) =>
>       (length(l) = n))))))
>
>[I am using the predicate symbol Item].  According to this axiom, taking
>n to be 1 and p to be hasFather, it suffices to show the existence of a
>non-repeating list l whose items are precisely the fathers of i, and
>then to show that this list has length 1.
>
>However, and here is the problem, all lists are finite, and it could be
>that i has infinitely many fathers.  In that case, there is no list l
>whose elements are precisely the fathers of i.  But if there are no such
>lists, it follows vacuously that all such lists are of length 1.  Hence
>the restriction does not rule out the case that i has infinitely many
>fathers.  In other words, as defined by the axiom, FatherClass contains
>elements which have either one father or infinitely many fathers.
>
>In practice, we can't use the cardinality axiom to show that there is a
>list l of length 1 having the desired property, since there might not be
>such a list.
>
>If it is the intention that the entire class of elements is finite, this
>is not expressed in the axioms.
>
>A similar problem may be expected to apply to other axioms for
>cardinality restrictions in DAML, such as maxCardinality, cardinalityQ,
>and maxCardinalityQ, which also use a non-repeating list which is
>supposed to contain all elements having a certain property.  It is
>possible that the axioms for minCardinality and minCardinaltyQ escape
>the problem, because the non-repeating list there is supposed to contain
>only a subset of the elements in question.
>
>Another problem is that the definition of NoRepeatsList(l) does not
>explicitly state that l must be a list.
>
>%% A NoRepeatsList is a list for which no item occurs more than once.
>(<=> (NoRepeatsList ?l)                          [NoRepeatsList axiom 1]
>     (or (= ?l nil)
>         (exists (?x) (= ?l (listof ?x)))
>         (and (not (item (rest ?l) (first ?l)))
>              (NoRepeatsList (rest ?l)))))
>
>
>There could be models in which a nonlist j, whose first is not a
>member of its rest and whose rest is equal to j itself, was a
>NoRepeatsList---this would not violate the axioms. Perhaps j = bottom
>is such an element.  The problem could be fixed by putting in a
>condition that l be a list, on the right hand side of the equivalence:
>
>
>(<=> (NoRepeatsList ?l)               [revised NoRepeatsList axiom 1]
>     (or (= ?l nil)
>         (exists (?x) (= ?l (listof ?x)))
>         (and (Type(?l, List))
>              (not (item (rest ?l) (first ?l)))
>              (NoRepeatsList (rest ?l)))))
>
>
>
>This being said, it may be a relief that the unrevised axioms do imply
>that every person has at least one father.  Here is the conjecture:
>
>
> conjecture people-have-at-least-one-father is
>  fa(c : Element)
>   Type(c, Person) =>
>   (ex(p : Element) HasFather(c, p))
>
>Here is a proof by SNARK, with my annotations:
>
>(Refutation
>
>The first two axioms are from the definition of FatherClass:
> (Row cardinality-of-fatherclass-is-one.7
>      (PropertyValue cardinality FatherClass 1)
>      assertion)
> (Row onproperty-of-fatherclass-is-hasfather.8
>      (PropertyValue onProperty FatherClass
>       hasFather)
>      assertion)
>
>This is part of the definition of Person, that it is a subclass of
>FatherClass:
> (Row person-in-fatherclass.9
>      (SubClassOf Person FatherClass)
>      assertion)
>
>Here are some basic axioms for lists and numbers:
> (Row nil-is-no-repeats-list.224
>      (NoRepeatsList nil)
>      assertion)
> (Row nothing-is-in-nil-Ax140.252
>      (not (Item nil ?Element))
>      assertion)
> (Row nil-is-a-list-Ax139.253
>      (Type nil List)
>      assertion)
> (Row zero-not-posnat.263
>      (not (= 0 ?Pos-Nat))
>      assertion)
>
>
>In SNARK notation, ?Pos-Nat is a variable of sort Pos-Nat---it ranges
>over positive integers.  Variables in assertions have tacit universal
>quantification.  Thus, the axiom zero-not-posnat says that zero is not
>equal to any positive integer.
>
>The theorem prover works by negating the theorem and finding a
>contradiction.  Hence it assumes that some element is a Person but does
>not have a father.  SK56 is taken to be one such element.
> (Row 218
>      (not (HasFather #Element-SK56 ?Element))
>      ~conclusion)
> (Row 219
>      (Type #Element-SK56 Person)
>      ~conclusion)
>
>
>Here is another property of lists, that a list has length 0 if it is
>nil.  Note that axioms are in clausal form;  implications P&Q => R are
>translated into (or (not P) (not Q) R):
>
> (Row length-nil.231-247
>      (or (not (Type ?Element List))
>          (= (length ?Element) 0)
>          (not (= ?Element nil)))
>      assertion)
>
>This is from the definition of SubClass:
> (Row definition-of-subclassof-Ax32.185-283
>      (or (not (SubClassOf ?Element ?Element1))
>          (not (Type ?Element2 ?Element))
>          (Type ?Element2 ?Element1))
>      assertion)
>
>This is a key axiom, from the definition of cardinality of
>restrictions;  ?Element stands for the restriction, ?Element1 stands
>for its onProperty:
>
> (Row definition-of-cardinality.70-417
>      (or (not (PropertyValue onProperty ?Element
>         ?Element1))
>      (not (PropertyValue cardinality ?Element ?Nat))
>      (not (Type ?Element2 ?Element))
>      (not (No-repeats-list ?Element3))
>      (PropertyValue item ?Element3
>        (#Element-SK9 ?Element3 ?Element1 ?Element2))
>      (PropertyValue ?Element1 ?Element2
>        (#Element-SK9 ?Element3 ?Element1 ?Element2))
>      (= (length ?Element3) ?Nat))
>         assertion)
>This says that the nonrepeating list of elements that satisfies the
>onProperty has length 1.
>
>This axiom lets us translate between formulas in terms of the constant
>hasFather and equivalent formulas in terms of the predicate symbol
>HasFather:
>  (Row hasfather-predicate-definition.11-458
>      (or (HasFather ?Element ?Element1)
>            (not (PropertyValue hasFather ?Element
>         ?Element1)))
>      assertion)
>
>Finally the proof begins; we translate the predicate symbol HasFather
>into the constant hasFather:
> (Row 470
>      (not (PropertyValue hasFather #Element-SK56
>     ?Element))
>      (negative-hyperresolve
>        hasfather-predicate-definition.11-458 218))
>
>Since Person is a subclass of FatherClass, SK-56 must be in FatherClass:
>
> (Row 472
>      (Type #Element-SK56 FatherClass)
>      (hyperresolve definition-of-subclassof-Ax32.185-283
>person-in-fatherclass.9 219))
>
>Since we have supposed that SK56 has no father, the list of its fathers
>must be nil; but by the cardinality restriction, this means that nil
>must have length 1:
> (Row 565
>      (= (length nil) 1)
>      (rewrite
>       (hyperresolve definition-of-cardinality-Ax113.70-417 472
>        onproperty-of-fatherclass-is-hasfather.8
>        cardinality-of-fatherclass-is-one.7
>        nil-is-no-repeats-list.224)
>       nothing-is-in-nil-Ax140.252 470))
>
>But this contradicts the fact that the length of nil is 0.
> (Row 1226
>      false
>      (rewrite (paramodulate length-nil.231-247 565)
>        nil-is-a-list-Ax139.253
>        zero-not-posnat.263
>        code-for-=))
> )
>
>
>To those who are interested in such things, here are some statistics
>from the SNARK proof search:
>
>;
>; Run time in seconds excluding printing time:
>;      2.9  41%   Resolution
>;      0.1   2%   Paramodulation
>;      0.1   1%   Factoring
>;      1.5  22%   Forward subsumption
>;      0.4   6%   Backward subsumption
>;      0.5   8%   Forward simplification
>;      0.0   1%   Backward simplification
>;      0.0   0%   Equality ordering
>;      0.2   3%   Sortal reasoning
>;      1.2  17%   Other
>;      7.0        Total
>
>The problem with the axiom doesn't affect this proof, since even if a
>person has infinitely many fathers, he or she still has at least one.
>
>My idea for fixing this problem involves introducing into the theory
>explicit sets, which may be finite or infinite.  Cardinality
>restrictions would then be expressed in terms of sets rather than
>nonrepeating lists.   But I am interested in hearing reactions before
>going ahead with this.  E.g., is this all wrong?
>
>---Richard W.

---------------------------------------------------------------------
(650)859 6569 w
(650)494 3973 h (until September)
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Thursday, 9 August 2001 19:27:10 UTC