W3C home > Mailing lists > Public > www-rdf-logic@w3.org > January 2001

Re: Bugs in 2000/12 daml+oil reference on DAML collections

From: Deborah McGuinness <dlm@ksl.stanford.edu>
Date: Tue, 16 Jan 2001 13:21:55 -0800
Message-ID: <3A64BB73.7497B0CD@ksl.stanford.edu>
To: Dan Connolly <connolly@w3.org>
CC: Ian Horrocks <horrocks@cs.man.ac.uk>, "Dickinson, Ian J" <Ian_J_Dickinson@hplb.hpl.hp.com>, www-rdf-logic@w3.org
Anotations below.

I think the axiomatic semantics has what is needed for list,
first, and rest .  I have grabbed the sections in the document and included
them in this note.

Please let me know if you think there are remaining issues.


Dan Connolly wrote:

deleting portions...

> Ian Horrocks wrote:
> >
> > On January 12, Dickinson, Ian J writes:
> >

> > 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.

in:  http://www.daml.org/2000/12/axiomatic-semantics.html

there is:
5.1.9.      List

%% “Seq” is a value of “subClassOf” for “List”.  (I.e., lists are sequences.)
Ax65.    (PropertyValue subClassOf List Seq)

5.2.22.  first

%% “first” is type “FunctionalProperty”.
Ax128.(Type first FunctionalProperty)

%% Saying that an object X is the value of “first” for an object L is
equivalent to saying that L is type “List” and the value of “_1” for L is X.
“first” is “_1” for lists.)
Ax129.(<=> (PropertyValue first ?l ?x)
                 (and (Type ?l List) (PropertyValue _1 ?l ?x)))

5.2.23.  rest

%% “rest” is type “FunctionalProperty”.
Ax130.(Type rest FunctionalProperty)

%% Saying that an object R is the value of “rest” for an object L is logically

equivalent to saying that L is type “List”, R is type “List”, and L has the
items in the same order as list R with one additional object as its first
Ax131.(<=> (PropertyValue rest ?l ?r)
                 (and (Type ?l List)
                      (Type ?r List)
                      (exists (?x) (= ?l (cons ?x ?r)))))[11]

%% Note that the following can be inferred from the axioms regarding “oneOf”,
“domain”, and “range”:
Th25.    (PropertyValue domain rest List))
Th26.    (PropertyValue range rest List)

Did someone think they needed more than this?

 Deborah L. McGuinness
 Knowledge Systems Laboratory
 Gates Computer Science Building, 2A Room 241
 Stanford University, Stanford, CA 94305-9020
 email: dlm@ksl.stanford.edu
 URL: http://ksl.stanford.edu/people/dlm/index.html
 (voice) 650 723 9770    (stanford fax) 650 725 5850   (computer fax)  801 705
Received on Tuesday, 16 January 2001 16:22:01 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:38:19 UTC