From: Richard Waldinger <waldinge@kestrel.edu>

Date: Fri, 03 Aug 2001 15:33:04 -0700

Message-ID: <3B6B26A0.F7D95AF1@kestrel.edu>

To: www-rdf-logic@w3.org

CC: Paul Kogut <paul.a.kogut@lmco.com>, Jeff Smith <composablelogic@mediaone.net>, Richard Waldinger <waldinger@AI.SRI.COM>, Ken Baclawski <kenb@ccs.neu.edu>, Mitch Kokar <kokar@coe.neu.edu>, "'Stephen Fitzpatrick'" <sfitzp@kestrel.kestrel.edu>, "andy.gurd" <andy.gurd@telelogic.com>, Jerzy Letkowski <jletkows@wnec.edu>, Cordell Green <green@kestrel.edu>, "Holmes III, William S" <william.s.holmes.iii@lmco.com>, "John J. Anton" <anton@kestrel.edu>, "Douglas E. Smith" <smith@kestrel.edu>, Mark Stickel <stickel@AI.SRI.COM>

Date: Fri, 03 Aug 2001 15:33:04 -0700

Message-ID: <3B6B26A0.F7D95AF1@kestrel.edu>

To: www-rdf-logic@w3.org

CC: Paul Kogut <paul.a.kogut@lmco.com>, Jeff Smith <composablelogic@mediaone.net>, Richard Waldinger <waldinger@AI.SRI.COM>, Ken Baclawski <kenb@ccs.neu.edu>, Mitch Kokar <kokar@coe.neu.edu>, "'Stephen Fitzpatrick'" <sfitzp@kestrel.kestrel.edu>, "andy.gurd" <andy.gurd@telelogic.com>, Jerzy Letkowski <jletkows@wnec.edu>, Cordell Green <green@kestrel.edu>, "Holmes III, William S" <william.s.holmes.iii@lmco.com>, "John J. Anton" <anton@kestrel.edu>, "Douglas E. Smith" <smith@kestrel.edu>, Mark Stickel <stickel@AI.SRI.COM>

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.Received on Friday, 3 August 2001 18:34:09 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Monday, 7 December 2009 10:52:40 GMT
*