For example, the value of the term (+ 2 3) is obtained by applying the addition function (the function denoted by +) to the numbers 2 and 3 (the objects denoted by the object constants 2 and 3) to obtain the value 5, which is the value of the object constant 5. If a functional term has a terminating sequence variable, the value is obtained by applying the function to the sequence of arguments formed from the values of the terms that precede the sequence variable and the values in the sequence denoted by the sequence variable.
Assume, for example, that the sequence variable @l has as value the sequence 2, 3, 4. Then, the value of the term (+ 1 @l) is obtained by applying the addition function to the numbers 1, 2, 3, and 4 to obtain the value 10, which is the value of the object constant 10.
The value of a logical term involving the if operator is the value of the term following the first true sentence in the argument list. For example, the term (if (> 1 2) 1 (> 2 1) 2 0) is equivalent to 2.
If none of the embedded sentences of a logical term involving the if operator is true and there is an isolated term at the end, the value of the conditional term is the value of that isolated term. For example, if the object constant a denotes a number, then the term (if (> a 0) a (- a)) denotes the absolute value of that number.
If none of the embedded sentences is true and there is no isolated term at the end, the value is undefined (i.e. bottom). In other words, the term (if (p a) a) is equivalent to (if (p a) a bottom).
The value of a logical term involving the cond operator is the value of the term following the first true sentence in the argument list. For example, the term (cond ((> 1 2) 1) ((> 2 1) 2)) is equivalent to 2.
If none of the embedded sentences is true, the value is undefined (i.e. bottom). In other words, the term (cond ((p a) a)) is equivalent to (cond ((p a) a) (true bottom)).
An inequality is true if and only if the terms in the equation refer to distinct objects in the universe of discourse.
If a relational sentence terminates in a sequence variable, the sentence is true if and only if the relation contains the tuple consisting of the values of the terms that precede the sequence variable together with the objects in the sequence denoted by the variable.
A conjunction is true if and only if every conjunct is true.
A disjunction is true if and only if at least one of the disjuncts is true.
If every antecedent in an implication is true, then the implication as a whole is true if and only if the the consequent is true. If any of the antecedents is false, then the implication as a whole is true, regardless of the truth value of the consequent.
A reverse implication is just an implication with the consequent and antecedents reversed.
An equivalence is equivalent to the conjunction of an implication and a reverse implication.
A simple universally quantified sentence (one in which the first argument is a list of variables) is true if and only if the embedded sentence is true for every value of the variables mentioned in the first argument.
Quantified sentences with complicated variables specifications can be converted into simple quantified sentences by replacing each complicated variable specification by the variable in the specification and adding an appropriate condition into the body of the sentence. Note that, in the case of a set restriction, it may be necessary to rename variables to avoid conflicts. The following pairs of sentences show the transformation from complex quantified sentences to simple quantified sentences.
(forall (... (?x r) ...) s)
(forall (... ?x ...) (=> (r ?x) s))
(exists (... (?x r) ...) s)
(exists (... ?x ...) (and (r ?x) s))
Note that the significance of free variables in quantifier-free sentences
depends on context. Free variables in an assertion are assumed to be
universally quantified. Free variables in a query are assumed to be
existentially quantified. In other words, the meaning of free variables is
determined by the way in which KIF is used. It cannot be unambiguously
defined within KIF itself. To be certain of the usage in all contexts, use
explicit quantifiers.
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.
The defobject operator is used to define objects. The legal forms are shown below, together with their content. In the first case, the content is the equation involving the object constant in the definition with the defining term. In the second case, the content is the conjunction of the constituent sentences.
(defobject s := t)
(= s t)
(defobject s p1 ... pn)
(and p1 ... pn)
(defobject s :-> v :=> p)
(=> (= s v) p)
(defobject s :-> v :<= p)
(<= (= s v) p)
The deffunction operator is used to define functions. Again, the
legal forms are shown below, together with their defining axioms. In the
first case, the content 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
content is the conjunction of the constituent sentences.
(deffunction f (v1 ...vn) := t)
(= (f v1 ...vn) t)
(deffunction f p1 ...pn)
(and p1 ...pn)
(deffunction f (v1 ... vn) :-> v :=> p)
(=> (= (f v1 ... vn) v) p)
(deffunction f (v1 ... vn) :-> v :<= p)
(<= (= (f v1 ... vn) v) p)
The defrelation operator is used to define relations. The legal
forms are shown below, together with their defining axioms. In the first case,
the content 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 content is the conjunction of the constituent sentences.
(defrelation r (v1 ...vn) := p)
(<=> (r v1 ...vn) p)
(defrelation r p1 ...pn)
(and p1 ...pn)
(defrelation r (v1 ... vn) :=> p)
(=> (r v1 ... vn) p))
(defrelation r (v1 ... vn) :<= p)
(<= (r v1 ... vn) p))