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

Assume, for example, that the sequence variable `@l` has as value the
sequence ` 2`,

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 (... (?xNote 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.r) ...)s) (forall (... ?x ...) (=> (r?x)s)) (exists (... (?xr) ...)s) (exists (... ?x ...) (and (r?x)s))

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.

(defobjectThes:=t) (=st) (defobjectsp1...pn) (andp1...pn) (defobjects:->v:=>) (=> (=psv)) (defobjectps:->v:<=) (<= (=psv))p

(deffunctionThef(v1...vn) :=t) (= (fv1...vn)t) (deffunctionfp1...pn) (andp1...pn) (deffunctionf(v1...vn) :->v:=>p) (=> (= (fv1...vn)v)) (deffunctionpf(v1...vn) :->v:<=p) (<= (= (fv1...vn)v))p

(defrelationr(v1...vn) :=p) (<=> (rv1...vn)p) (defrelationrp1...pn) (andp1...pn) (defrelationr(v1...vn) :=>) (=> (prv1...vn))) (defrelationpr(v1...vn) :<=) (<= (prv1...vn)))p

Michael R. Genesereth