Deborah, you asked for comments. 


First, a comment on terminology. Maybe it is too late to stop this
usage, but (as I am sure you know), what you have written is not, in
fact, a model-theoretic semantics for DAML, but a transcription of DAML
into a language which has a model-theoretic semantics.  This is only a
terminological issue, but it does mean that if we all adopt this new
usage of "model theoretic semantics", there will be no way to refer to
an actual model theoretic semantics unless we invent a new word. Since
this particular terminology has been in settled use throughout logic
and philosophy of language for about 55 years it seems a pity to create
new confusions by being careless with it.


1. I think the following is slightly incorrect:


<bold><fontfamily><param>Courier_New</param>%% The first argument of
"intersectionOf" is the intersection of the classes in the list that is
the second argument of "intersectionOf".

(<<=> (intersectionOf ?c1 ?l)

     (<<=> (type ?x ?c1) 

          (forall ?c2 (=> (item ?c2 ?l) (type ?x ?c2 )))))


</fontfamily></bold>and I think the formula should read 


<bold><fontfamily><param>Courier_New</param>(<<=> (intersectionOf ?c1
?l)

     (forall (?x)(<<=> (type ?x ?c1) 

          (forall ?c2 (=> (item ?c2 ?l) (type ?x ?c2 ))))) )


</fontfamily></bold>2. A slight KIF typo:


<bold><fontfamily><param>Courier_New</param>%% The complement of a
class is the class of objects that are not instances of the class.

(<<=> (complementOf ?c1 ?c2)

     (and (disjointWith ?c1 ?c2) 

          (forall ?x (or (type ?x ?c1) (type ?x ?c2)))))


</fontfamily></bold>should read:

<bold><fontfamily><param>Courier_New</param>(<<=> (complementOf ?c1
?c2)

     (and (disjointWith ?c1 ?c2) 

          (forall (?x) (or (type ?x ?c1) (type ?x ?c2)))))


</fontfamily></bold>The quantified variable must be enclosed in
brackets.


3.  Similarly to 1., 


<bold><fontfamily><param>Courier_New</param>%% "oneOf" enumerates the
instances of a class.

(<<=> (oneOf ?c ?l) (<<=> (type ?x ?c) (item ?x ?l)))


</fontfamily></bold> should read:


<bold><fontfamily><param>Courier_New</param>(<<=> (oneOf ?c ?l)(forall
(?x)(<<=> (type ?x ?c) (item ?x ?l))))


</fontfamily></bold>4. You define 'asClass' as identity restricted to
classes. But there is no need to restrict it to classes, since a class
cannot be identical to a nonclass. You can just treat 'asClass' as
simple identity. (Maybe this is why the spec didn't bother to define
it?)


5. While the following is indeed legal KIF:


<bold><fontfamily><param>Courier_New</param>%% The second argument of
"first" is the first item on the list that is the first argument of
"first".

(<<=> (first ?l ?x) (exists @r (= ?l (listof ?x @r))))


</fontfamily></bold>it is likely that sequence variables will be
abandoned in the new standard, so I would suggest an alternative
axiomatisation using LISP cons:


<bold><fontfamily><param>Courier_New</param>(<<=> (first ?l ?x) (exists
(?r) (= ?l (cons ?x ?r))))


</fontfamily></bold>A similar method can be used to modify the axiom
for 'rest'.


6. Re. the use of 'holds', it is likely that the new standard will
allow variables to be used in the relation position, making 'holds'
unneccessary. 


Pat  

---------------------------------------------------------------------

IHMC					(850)434 8903   home

40 South Alcaniz St.			(850)202 4416   office

Pensacola,  FL 32501			(850)202 4440   fax

phayes@ai.uwf.edu	                          http://www.coginst.uwf.edu/~phayes