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 .