- From: Dan Connolly <connolly@w3.org>
- Date: Fri, 12 Jan 2001 12:16:02 -0600
- To: Ian Horrocks <horrocks@cs.man.ac.uk>
- CC: "Dickinson, Ian J" <Ian_J_Dickinson@hplb.hpl.hp.com>, www-rdf-logic@w3.org

Ian Horrocks wrote: > > On January 12, Dickinson, Ian J writes: > > I'll skip the stuff about typos in the reference document > > [snip] > > Good point about Disjoint. > > The reason for the different use of List in Disjoint and oneOf is that > Disjoint is an axiom that makes an assertion about the elements of the > list, but which does not define a new class. Note that this affects > the semantic interpretation of each of the elements, but daml+oil does > not assign any semantics to the Disjoint class itself. I'm not sure what you mean by that; we the relevant axiom is just as much about the Disjoint class as about the classes inside a Disjoint: Ax56. (<=> (Type ?l Disjoint) (and (Type ?l List) (forall (?c) (=> (PropertyValue Item ?c ?l) (Type ?c Class))) (forall (?c1 ?c2) (=> (and (PropertyValue item ?c1 ?l) (PropertyValue item ?c2 ?l) (not (= ?c1 ?c2))) (PropertyValue disjointWith ?c1 ?c2))))) -- http://www.daml.org/2000/12/axiomatic-semantics.html > > oneOf is not, by itself, an axiom: it is a class constructor. What's a class constructor? oneOf is just a property; it relates a class, say C, and a list, say L; it says that something is in C (i.e. related to C by rdf:type) exactly when it's in L (i.e. related to L by daml:item). The relevant axiom is: Ax84. (<=> (PropertyValue oneOf ?c ?l) (and (Type ?c Class) (Type ?l List) (forall (?x) (<=> (Type ?x ?c) (PropertyValue item ?l ?x))))) > It > builds a new class from the elements of the List and, only when it is > used as a property of a class C do we have an axiom asserting that the > interpretation of C is the same as the interpretation of the class > built by oneOf. > > However, this doesn't solve the problem with the daml:collection parse > type. If daml:collection turns the enclosed elements into a List > structure, then it doesn't make sense to use it inside another list > without an intervening property. I don't like using equivalentTo (as > suggested by Dan) I don't find it syntactically appealing, but it works; equivalentTo can always be used as a syntactic shim to relate two terms that denote the same thing, no? > as the List itself doesn't have any semantics, Huh? List/first/rest have the usual semantics; e.g. (forall (?l1 ?l2 ?f ?r) (=> (and (daml:List ?l1) (daml:List ?l2) (daml:first ?l1 ?f) (daml:rest ?l1 ?r) (daml:first ?l2 ?f) (daml:rest ?l2 ?r)) (daml:equivalentTo ?l1 ?l2) ) isn't that in the axiomatic semantics? (I've left out the Type and PropertyValue thingies; and daml:equivalentTo is interchangeable whith KIF's = yes, that's explicit: Ax68) http://www.daml.org/2000/12/axiomatic-semantics.html Ugh.. I don't see any axioms about first/rest there; Let's please add it. > so its hard to see how it can be equivalent to anything. Why? Even without list semantics, I can take any two terms and say they're daml:equivalentTo each other, no? > I would > suggest that a better way to do it would be: > > <daml:Disjoint> > <daml:first rdf:resource="#Car"/> > <daml:rest rdf:parseType="daml:collection"> > <rdfs:Class rdf:about="#Person"/> > <rdfs:Class rdf:about="#Plant"/> > </daml:rest> > </daml:Disjoint> That works too. > > Regards, Ian > > > The second problem is that it would be nice if we could apply a simple > > syntactic transformation [...] -- Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Friday, 12 January 2001 13:17:19 UTC