Re: An ontology for KIF

Tom Gruber <Gruber@HPP.Stanford.EDU>
Full-Name: Tom Gruber
Message-id: <2954638997-7619985@KSL-Mac-69>
Date: Tue, 17 Aug 93  22:03:17 PDT
From: Tom Gruber <Gruber@HPP.Stanford.EDU>
To: interlingua@ISI.EDU
Subject: Re: An ontology for KIF
References: <>,
In-reply-to: Msg <> from macgregor@ISI.EDU
Messages from Macgregor, Fulton, Hayes, and Ginsberg have all been
about what some have been calling "Representation Ontologies" -
specifications of conceptualizations that are so general that
they find themselves in the very kernel of knowledge representation
languages.  Why they are built in to KR languages, and the role of
such ontologies in knowledge interchange, is the issue at hand.  
A few comments.


KIF has, built in, several ontologies; in fact the bulk of the 3.0
spec is devoted to the ontologies for sets, sequences, numbers,
relations, and expressions, not the core syntax and semantics.

The specifications of KIF's ontologies are available online in the knowledge sharing
"ontologies" library 

Each ontology is a set of definitions, given in a mix of english prose
and KIF axioms, that specify (and give names for) the individuals and
relations that matter for some domain of discourse.  If you throw away
the prose, you get a set of axioms, which of course describes a
theory.  \Tangent{So those who dislike pronouncing the word "ontology"
can substitute "theory" throughout.  In my book, an ontology is a
specification of a conceptualization, and axioms are one way to help
make the specification clear and coherent.}

These ontologies are built into KIF because most of them have some
link to the syntax and semantics of KIF.  (The exception is numbers,
which is yet to be formalized).  For example, "setofall" is mentioned
in the BNF syntax, and it is the hook that links predication to sets.
Yet most of the definitions in the sets ontology are just a routine
axiomatization of set theory.  They are needed because KIF makes a
commitment to sets in its syntax and semantics.  Similarly, KIF needs
a theory of sequences because of the syntax for sequence variables
(those that start with "@") and the semantics of KIF expressions as

Same for relations.  KIF needs the relations ontology (which defines
relations as sets of tuples) because the definitions of the lambda,
kappa, holds, and values operators depend on this axiomization of
relations.  The fact that function constants can be used in the
relational position as predicates depends on the axiom that functions
are a special case of relations.


Some representation ontologies are not strictly necessary for KIF, but
are useful for translation.   The frame ontology, for example, is an
extension of KIF's relations ontology that brings in the notion of
class (as a unary relation) and defines a family of second-order
relations such as those used in frame systems to specify slot
cardinality and type constraints.   The frame ontology is designed
specifically to allow for translation among object-centered knowledge
representations.   In fact, what macgregor asked for:

   (1) distinguishing between "types" and "properties" (or between
       "types" and other unary relations);
   (2) providing for terms that denote slots/roles (noting that in many
       or most frame systems, there can be many slot/role objects that 
       all correspond to the same binary relation);
   (3) allowing classes and higher-arity relations to have overlapping
       name spaces;
   (4) frame predicates (e.g., "single-valuedness", "symmetry", etc).

can be done with some minor revisions to the frame ontology.
Interested parties, including some of the people mentioned above, are
involved in ontology design discussions for this purpose.  You are
welcome to take a look and the existing frame ontology and comment.
The frame ontology is in the same ftp directory mentioned above.
(Each ontology is available in several languages: KIF wrapped in
Ontolingua forms (.lisp), pure KIF (.kif), a object-oriented syntax
(.gf), Epikit (.epikit), and an incomplete translation into Loom


--- Excerpt from pat hayes (Mon, 16 Aug 93 14:33:50 -0800) ---

> But the issue is whether the ontology
> has a special relationship to the syntax. The distinction between type and
> unary-predicate has no semantic content in the usual semantics of KIF, so can't
> be captured in an ordinary ontology: but some systems need to have it
> maintained. So, some predicates have to be specially marked as type-ish. But
> this kind of 'marking' seems to involve a different kind of relationship between
> (an aspect of) KIF syntax and a predicate (specifically, the "Type" predicate)
> than the usual kind of relationship. This is a change (extension) to the logic,
> and should really be treated like one: but in any case, it can't be captured by
> an ordinary first-order theory (whoops, sorry, ontology).

Let's say a logic has a syntax that requires that all quantification
be typed.  In that logic, the sentence

  (forall ((?x Tx) (?y Ty)) (p ?x ?y))

Means "forall ?x's of type Tx and ?y's of type Ty, P of ?x ?y holds."

This would translate into KIF 3.0 as 

  (forall (?x ?y) (=> (and (Tx ?x) (Ty ?y)) (p ?x ?y)))

Now, what I think Sowa and MacGregor and others want is a way to tag
the Tx and Ty relations as types, distinguishing them from other
relations that, for instance, you wouldn't quantify over in natural
language (e.g., "forall red things, ...").  One could define a
second-order relation called TYPE, and assert (type Tx).

As Pat points out, KIF's theory of relations doesn't offer any
machinery with which to formally distinguish types from other unary
relations.  However, that doesn't mean that we can't define the TYPE
relation as a primitive, just as KIF defines SET as a primitive.  In
such a definion, a type could be defined as a unary relation
(=> (unary-relation ?r) (type ?r)) that also has this property that
we can't define using the existing KIF primitives.  Assuming we could
give an adequate account of its meaning in prose -- a meaning that did
not depend on having a computer program in hand or having been
educated at a particular institution -- then it would be as legitimate
a definition as KIF's definition of SET.

An ontology that defines the type relation, combined with other
representation ontologies such as KIF's relations and the frame
ontology, could be a basis for translating among all those systems
that are consistent with the definitions in the ontology.  The meaning
of this TYPE predicate would not be tied to the _syntax_ of KIF or any
of the languages, only to an assumption about a conceptualization
(i.e., that there is a distinction between a type and a unary
relation).  Specifying these assumptions about the modeled world is
what ontologies do for a living.