Re: A Model Theoretic Semantics for DAML-ONT

Pat,

I also like that approach, and I think it can be done in way
that satisfies the B2B people:

>Yet another strategy (which I myself prefer) is to simply remove the 
>concept of 'definition' from KIF altogether, treat all definitions as 
>simply assertions of biconditionals, and stick strictly to the Caveat 
>Orator principle. But I can see that this might not be acceptable in 
>B2B semantic-web kinds of application.

The difference between a definition and a biconditional cannot
be expressed in a pure FOL at the object level.  However, it can
be expressed at the metalevel, including a metalevel that uses
FOL to talk about a domain that includes expressions.

At the metalevel, you would need an assert statement to enter
new statements into the current KIF "workspace" or "context".
And when you assert a proposition ?p, you would add another
statement that explains who was the authority for ?p:

   (and (assert ?p)
        (authorityFor ?p "Pat Hayes"))

Then you could define a hierarchy of authorities, with God
(or BuiltInDefiner) at the top.  That definition, of course,
would be asserted as a biconditional at the metametalevel,
with the appropriate god or gods as authority.

John