Amendment to KIF's unary-relation and binary-relation

macgregor@ISI.EDU
Message-id: <199308252040.AA04880@quark.isi.edu>
Date: Wed, 25 Aug 1993 13:39:27 -0800
To: interlingua@ISI.EDU
From: macgregor@ISI.EDU
Subject: Amendment to KIF's unary-relation and binary-relation


Apparently, I failed for some time to read some of the fine print in
the KIF document, and I've only just discovered a new problem with it. The
definitions of unary-relation and binary-relation include a "non-empty"
clause, e.g., it is supposed to be impossible to define a non-empty
unary-relation in KIF. This restriction needs to be remedied.

The principal problem with the current document is that
"unary-relation" and "binary-relation" as currently defined have
unreasonably low applicability. Suppose I have a knowledge base
consisting of the single statement

   (defrelation A (?a) :=> (Thing ?a))

(I am assuming that a top-level concept "Thing" is built-in to
the system, but thats not really relevant).  Is "A" a unary-relation?
Well, we can't tell, since we have no axioms available asserting
that A is not empty.  That means among other things that we cannot
confidently translate the definition of "A" into a Loom "defconcept" 
or to some other frame system's equivalent of "defclass".

The current definition also means that we would be incautious if we
were to incorporate "unary-relation" into a sugar-coated construct like
Ontolingua's "define-class", i.e., the statement

   (define-class A (?a) :def (Thing ?a))

ought not to presume that instances that satisfy "A" necessarily
exist (currently Ontolingua does presuppose the existence of 
members of its classes -- this is unfortunate).

I propose that unary-relation and binary-relation be redefined in KIF
as partial relations that DO NOT imply that their arguments are
non-empty, i.e., define them as follows:

   (defrelation unary-relation (?r)
       :=> (forall (?l) (=> (member ?l ?r) (single ?l))))
   (defrelation binary-relation (?r)
       :=> (forall (?l) (=> (member ?l ?r) (double ?l))))

With this redefinition, it is still the case that the bare definition
   (defrelation A (?a) :=> (Thing ?a))
cannot be interpreted as a definition of a concept A, but we can
assume that an accompanying axiom  (unary-relation A) would
be generated by translators that translate concepts into KIF.

Next, I would prefer that the property of being a unary- or binary-relation
be considered analytic.  However, this may not matter to KIF.  Using
the amended definition for "unary-relation" I can correctly translate
the Loom statement
   (defconcept A :is-primitive Thing)
into KIF as
   (defrelation A (?a) :=> (Thing ?a))
   (defining-axiom 'A '(unary-relation A))

This raises a question about defining axioms.  If a constant is
bound to multiple defining axioms, is that equivalent to stating
a single defining axiom that and's together all of the others?  For
example, are the two KIF statements just above equivalent to 
   (defining-axiom 'A
     '(and (=> (member ?t A) (= (length ?t) 1))
           (=> (A ?x) (Thing ?x))
           (unary-relation A)))
?            
       
Cheers, Bob

Robert M. MacGregor                                     macgregor@isi.edu
USC/ISI, 4676 Admiralty Way, Marina del Rey, CA 90292      (310) 822-1511