- From: Richard Waldinger <waldinger@AI.SRI.COM>
- Date: Fri, 14 Sep 2001 13:01:49 -0700
- To: Richard Fikes <fikes@KSL.Stanford.EDU>
- CC: "www-rdf-logic@w3.org" <www-rdf-logic@w3.org>, Pat Hayes <phayes@ai.uwf.edu>
Your new axioms look plausible to me. I'll try putting the cardinality
axiom into the Specware theory next week and see if SNARK can prove the
desired results.
Three comments:
* You put the quantifier for ?m into the definition of maxCardinality,
but you forgot to put it into the definition of cardinality.
* I still don't think you need to change the definition of
NoRepeatsList to have a second argument, the length of the list. You
could use the original definition and make the axiom be
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue cardinality ?r ?n))
(forall (?i)
(<=> (Type ?i ?r)
(exists (?vl ?m)
(and (NoRepeatsList ?vl)
(= (length ?v1) ?m)
(forall (?v)
(<=>
(PropertyValue item ?vl
?v) (PropertyValue ?p ?i ?v))))))))
* It might still be closer to intuition to use sets rather than
NoRepeatsList.
The axiom would then read
(=> (and (PropertyValue onProperty ?r ?p)
(PropertyValue cardinality ?r ?n))
(forall (?i)
(<=> (Type ?i ?r)
(exists (?vl ?m)
(and (Type ?vl Set)
(= (card ?v1) ?m)
(forall (?v)
(<=>
(PropertyValue item ?vl
?v) (PropertyValue ?p ?i ?v))))))))
You could remove the axioms for NoRepeatsList and length, but would need
to add the axioms for (at least finite) sets and card. This seems to me
closer to the way we would describe the definition in conversation, say,
but the argument is not so compelling if we can avoid talking about
infinite sets.
I'll report on whether the proofs work.
---Richard W.
Received on Friday, 14 September 2001 16:03:19 UTC