Definitions



next up previous
Next: Numbers Up: Semantics Previous: Nonmonotonic Entailment

Definitions

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


(defobject := )&(= )&(defobject ... )&(and ... )

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


(deffunction ( ...) := )&(= (lambda ( ...) ))&(deffunction ... )&(and ... )

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


(defrelation ( ...) := )&(= (kappa ( ...) ))&(defrelation ... )&(and ... )

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



next up previous
Next: Numbers Up: Semantics Previous: Nonmonotonic Entailment



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994