- From: Richard Waldinger <waldinger@AI.SRI.COM>
- Date: Tue, 25 Sep 2001 17:35:22 -0700
- To: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>
The revised axiom Richard Fikes proposed for the cardinality restriction succeeded in allowing proofs of a number of expected properties of the construct. While I had proposed introducing a comprehension axiom, which says that a list (or set) exists that contains all elements that satisfy certain properties, the new axiom avoids any such requirement. The axiom is formulated in terms of NoRepeatLists --- I think it might be slightly simpler if formulated in terms of sets, but that would require introducing axioms for sets as well as lists. The revised theory, like the original one, is agnostic about whether some lists are infinite or all lists are finite. The revised theory also avoids versions of Russell's paradox that threatened formulations that contained a comprehension axiom. The new theory has defeated earnest attempts (5 CPU hours) to find contradictions. The validation of the revised theory was carried out using theory-manipulation facilities of Specware --- proofs were done by the theorem prover SNARK, which is embedded in Specware. The revised axiom says that if restriction r has onProperty p and cardinality component n, then an element i is in r iff some NoRepeatsList that contains precisely the values of p on i has length n. In Specware notation, this is axiom definition-of-cardinality-revised is fa(r : Element, p : Element, n : Nat) ((PropertyValue(onProperty, r, p) & PropertyValue(cardinality, r, n)) => (fa(i : Element) (Type(i, r) <=> (ex (v1 : Element) (NoRepeatsList(v1) & length(v1) = n) & (fa(v : Element) (Item(v1, v) <=> PropertyValue(p, i, v))))))) The earlier axiom said that i is in the restriction r iff *every* NoRepeatsList that contains precisely the values of p on i has length n: axiom definition-of-cardinality-Ax113 is fa(r : Element, p : Element, n : Nat) ((PropertyValue(onProperty, r, p) & PropertyValue(cardinality, r, n)) => (fa(i : Element) (Type(i, r) <=> (fa(vl : Element) ((NoRepeatsList(vl) & (fa(v : Element) (Item(vl, v) <=> PropertyValue(p, i, v)))) => (length(vl) = n)))))) The chief difference between these is that the earlier axiom says that every list having the right elements has length n. The new axiom says that there exists a list of the right elements with length n. The earlier axiom left open the possibility that no list exists that has the right elements. Since the new axiom implies that there exists a list with the right elements, there is no need to prove it. The validation was carried out on a particular example: we define a restriction OneFatherClass that is intended to consist of all elements with precisely one father: axiom onproperty-of-onefatherclass-is-hasfather is PropertyValue(onProperty,OneFatherClass, hasFather) axiom cardinality-of-onefatherclass-is-one is PropertyValue(cardinality, OneFatherClass, _1) The class Person of all people is asserted to be a subclass of this restriction class: axiom restriction-subclass-of-class-Ax55 is PropertyValue(subClassOf, Restriction, Class) This example was obtained from the DAML Walkthru document, http://www.daml.org/2001/03/daml+oil-walkthru.html . We expect to be able to prove the following claims: If an element has precisely one father, then it is in the OneFatherClass; i.e., conjecture one-father-in-onefatherclass is fa(c : Element, p1 : Element) (fa(p : Element)(PropertyValue(hasFather, c, p) <=> p = p1)) => Type(c, OneFatherClass) Every person has at least one father; i.e., conjecture people-have-at-least-one-father is fa(c : Element) Type(c, Person) => (ex(p : Element) PropertyValue(hasFather, c, p)) No person has two distinct fathers; i.e., conjecture people-have-at-most-one-father is fa(c : Element, p1 : Element, p2 : Element) Type(c, Person) & PropertyValue(hasFather, c, p1) & PropertyValue(hasFather, c, p2) => p1 = p2 The original axiom did not imply this last property; with the new axiom Specware/SNARK can prove all of them. Copies of the theory slice, which contains all the axioms and lemmas necessary to prove the desired properties, are available on request.
Received on Tuesday, 25 September 2001 20:36:01 UTC