Comments on neww KIF Manual

Robert MacGregor <macgreg@ISI.EDU>
Message-id: <199206091635.AA19860@quark.isi.edu>
To: Richard Fikes <fikes@sumex-aim.stanford.edu>
Cc: interlingua-working-group@ISI.EDU
Reply-To: macgregor@ISI.EDU
Subject: Comments on neww KIF Manual
Date: Tue, 09 Jun 92 09:35:22 PDT
From: Robert MacGregor <macgreg@ISI.EDU>


This version of KIF is a big improvement over the
previous version.  Below are my comments.

Tiny bug: page 11: the word "forward" in the phrase
"forward rule" is undefined.

Tiny bug2: page 22: a few $x variables should be ?x.

Lists, p. 31.  Definitions (6.7), (6.8) and elsewhere,
include unquantified sequence variables within a
definition.  The document defines what it means for
a variable to be unquantified within a sentence, but I
don't see anything that defines how an unquantified variable
is to be interpreted within a definition.

Equality for lists.  The document defines what it means for
two sets to be equal, but I don't see where it defines
equality over lists, i.e., if ?l1 and ?l2 are bound to
two lists, there are no axioms for evaluating
(= ?l1 ?l2), except when they are both nil.  Perhaps this
is deliberate.  If so, it might be worthwhile to explain
why within in the document.

Sets, p.34.  You state that it is "fortunate" that there are
multiple mathematical theories for formalizing the semantics of
sets.  Actually, it is unfortunate.  If everyone's KR system
chose the same set theory, then the existence of multiple
theories would merely be a curiousity, but in reality it is a
problem.  I have no quibble with your choice of the von
Neumann-Bernays-Goedel set theory, but there are KR systems that
make a different choice, e.g., some of the description logic (DL)
systems are moving in the direction of Aczel's axiomiatization.
In the old KIF, the answer would be for everyone to state their
own axiomatization in a preamble to the main kb.  The new answer,
which I like better, is that KIF comes with a built-in
semantics.  However, it is not clear to me how KIF is supposed
to accomodate semantics that differ from its own.  Perhaps a
later version of the document will illustrate how one does that.

Fixed-point semantics.  For KIF's defxxx operators to have a
well-defined semantics, you need to specify a fixed point
semantics.  I assume that you are adopting a least fixed point
semantics, and I believe that I saw a reference to such, but I
can't find it again.  Wherever that reference is, it should be
made more visible.  The description logic community seems to be
unsettled as to whether it prefers a greatest fixed point semantics
or a descriptive semantics for defining concepts/relations.  In
any case, it seems to have rejected least fixed point semantics.
This does not mean that KIF should do the same, but it does mean
that there is no obvious translation of a DL into KIF.  We need
to come up with a methodology that describes how this can
be accomplished.

Tiny bug:  (9.16) the word "quoterm" is missing.

p.62 "The defining axiom essentially states that if an entity
exists in the domain of discourse having all ...  then the constant
denotes such an entity ..." Suppose two domain entities exist that
both satisfy all properties ascribed to the constant -- which of
them does the constant denote?  Possibly you mean to say "if a UNIQUE
entity exists in the domain ...".

To be consistent with KIF's preference for variable arity relations,
the "composition" relation should support variable arity rather
than just binary inputs.

Propositions.  I believe Richard mentioned that he was working on a
representation for propositions.  Perhaps their introduction into
KIF 3.0 is premature, but I think they need to appear eventually.  I
believe that I am not alone in considering a proposition rather
than a sentence to be the most appropriate argument for a
"believes" relation.  From this perspective, the examples in
Chapter 9 are misleading, since they suggest that applying a
"believes" operator to a quoted sentence is appropriate.  The best
stance for KIF to take would be neutrality, rather than implicitly
stating a preference for sentences as objects of belief.  I would
recommend inserting a statement that a future version of KIF will
include a representation for propositions.

The document badly needs an index.

All in all, though, I like this version of KIF.  The notion of a
partial definition as an alternative to primitiveness presumably
needs a blessing by others in the description logic community, but
it looks fine to me.  I consider the KIF notion of "defining
axioms" to be an improvement on the more narrow notion of
definition currently espoused by DL folks.  The gap between
relations and functions has been reduced to a point where its now
completely compatible with my own preferences.

What is missing from KIF is any notion of intensional entities.
For example, KIF's semantics for relations are extensional -- I
assume that KIF considers the concept of a Three-Sided Square to be
equivalent to the concept of a Round Square, since they both have
null extensions.  If and when we consider propositions, the same
questions of equivalence will surface.

Also, KIF does not contain anything resembling the frame notion of
"role".  I am curious to know how a role in Ontolingua is translated
into KIF.  Perhaps propositions and roles move us from the
realm of KIF to ontology?

Cheers, Bob