The definitional operators in KIF allow us to state sentences that are true ``by definition'' in a way that distinguishes them from sentences that express contingent properties of the world. Definitions have no truth values in the sense described above. They are so because we say that they are so.

On the other hand, definitions have content - sentences that allow us to derive
other sentences as conclusions. In KIF, every definition has a corresponding
set of sentences, called the *content* of the definition. In general, there are
three parts to this content.

First of all, there is information about the category of the constant in the definition. If the constant is a function constant or a relation constant, there is also information about its arity.

Second, there is the *defining axiom* associated with the definition (see
below).

Finally, there is a sentence stating that the defining axiom associated with the definition is indeed a defining axiom for the associated concept (named by the constant used in the definition). The following sentence expresses this fact. Note the use of quotes to capture the fact that this is a relationship between a constant and a sentence.

`(defining-axiom ' ')`

The rules for determining the defining axioms for a definition are somewhat complicated and are described fully in the chapter on definitions. The following is a brief outline, sufficient to enable the reader to understand the use of definitional constructs in the intervening chapters.

The `defobject` operator is used to define objects. The two simplest forms are
shown below, together with their defining axioms. In the first case, the defining
axiom is the equation involving the object constant in the definition with the
defining term. In the second case, the defining axiom is the conjunction
of the constituent sentences.

#&#Definition&Defining Axiom

The `deffunction` operator is used to define functions. Again, the two simplest
forms are shown below, together with their defining axioms. In the first case, the
defining axiom is the equation involving (1) the term formed from the function constant
in the definition and the variables in its argument list and (2) the defining term. In
the second case, as with object definitions, the defining axiom is the conjunction of
the constituent sentences.

#&#Definition&Defining Axiom

The `defrelation` operator is used to define relations. The two simplest forms are
shown below, together with their defining axioms. In the first case, the defining
axiom is the equivalence relating (1) the relational sentence formed from the relation
constant in the definition and the variables in its argument list and (2) the defining
sentence. In the second case, as with object and function definitions, the defining
axiom is the conjunction of the constituent sentences.

#&#Definition&Defining Axiom

For most purposes, a definition can be viewed as shorthand for the sentences in the content of the definition.

Wed Dec 7 13:23:42 PST 1994