KIF includes a set of definition operators for declaring the category and
defining axioms (e.g. ``Triangles have 3 sides.'') for constants. Such *analytic definitions* are intended for use in specifying representation and
domain ontologies, and are in contrast to metalinguistic *substitutional
definitions* that specify new object level syntax in a macro-like
fashion.KIF 3.0 does not provide facilities for substitutional
definitions. Consideration is being given to including them in later versions
of the language. KIF definitions can be *complete* in that they specify an
expression that is equivalent to the constant, or *partial* in that they
specify a defining axiom that restricts the possible denotations of the
constant. Partial definitions can be either *unrestricted* or *conservative*
extensions to the language. Conservative definitions are restricted in that
adding the defining axioms they specify to any given collection of sentences
not containing the constant being defined does not logically entail any
additional sentences not containing the constant being defined. [Enderton
72].

An analytic definition associates with the constant being defined a *defining axiom*. Intuitively, the meaning of a definition is that its
defining
axiom is true and that its defining axiom is an *analytic truth*.
Analytic
truths are considered to be those sentences that are logically entailed from
defining axioms. For example, term subsumption in the KL-ONE family of
representation languages is an analytic truth in that it is determined solely
on
the basis of term definitions. The notions of defining axiom and analytic
truth are formally defined as follows.

Given a knowledge base , the sentence `(defining-axiom '
')` means that there is in an analytic definition of constant
which specifies sentence as a defining axiom of constant .
Moreover, defining axioms are true. That is, the following axiom schema
holds:

`(=> (defining-axiom ' ') )`

Given a knowledge base , the sentence `(analytic-truth ')`
means that the sentence is logically entailed by the defining axioms of
the definitions in knowledge base .

Wed Dec 7 13:23:42 PST 1994