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

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. thx, Deborah 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) and 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 logically equivalent to saying that L is type “List” and the value of “_1” for L is X. (I.e., “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 same items in the same order as list R with one additional object as its first item. 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 0941Received 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
*