Given an interpretation and a variable assignment, we can assign a *semantic value* to every term in the language. We formalize this as a
function from the set of terms into the set
of objects in the universe of discourse.

If an expression is an individual variable

, the semantic value is the object assigned to that variable by the given variable assignment.

The semantic value of an object constant

is the object assigned to that constant by the given interpretation.

The semantic value of a function constant

is the set of tuples in the universe of discourse corresponding to the function denoted by

. Here, we use the
operator `lambda` to denote this function. A full description of the semantics of
expressions involving `lambda` is given later.

The semantic value of a relation constant

is the set of tuples in the universe of discourse corresponding to the relation denoted by

. Here, we use the
operator `kappa` to denote this relation. A full description of the semantics of
expressions involving `kappa` is given later.

In most cases, the semantic value of a function or relation constant is the same as its interpretation. However, in order to avoid paradoxes, it must in some cases be different. See the chapter on sets for a fuller discussion of this subject.

The semantic value of a functional term without a terminating sequence variable is obtained by applying the function denoted by the function constant in the term to the objects denoted by the arguments.

If a functional term has a terminating sequence variable, the semantic 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. (The vertical bar

here means that the objects in the sequence following the bar are appended to the sequence of elements before the bar.)

A term that begins with *listof* refers to the sequence of objects
denoted by the arguments in the term. There is no restriction on the
objects in the sequence.

If a term that begins with `listof` ends with a sequence variable,
the value of the term as a whole is the sequence consisting of the
objects denoted by the terms prior to the sequence variable together
with the objects in the sequence denoted by the sequence variable.

A term that begins with *setof* refers to the set of ``bounded''
objects denoted by the arguments in the term. The concept of
boundedness is discussed further in the chapter on sets.

If a term that begins with `setof` ends with a sequence variable, the value of
the term as a whole is the set consisting of the bounded objects denoted by the terms
prior to the sequence variable together with the bounded objects in the sequence
denoted by the sequence variable.

A quotation denotes the expression contained as argument of the `quote`
operator. Remember that the universe of discourse for every interpretation
must contain all list expressions and that the argument to `quote` can be
any list expression, whether or not it is a legal expression in KIF.

Note that any KIF expression (other than a word) is a sequence of KIF expressions.
Thus, there are two ways it can be denoted - with `quote` and with `listof`. This means we have the following equivalence.

The semantic value of a simple conditional term depends on the truth value of the embedded sentence (see next section). If the truth value of the embedded sentence is

, then the semantic value of the term as a whole is the semantic value of the first term; otherwise, it is the semantic value of the second term (if there is one).

If a simple conditional has only one embedded term and the truth value of the embedded sentence is

, then the semantic value of the term is the semantic value of the embedded term. Otherwise, the value is

.

The semantic value of a complex conditional is the semantic value of the *first* term for which the truth value of the corresponding sentence is

. If none of the sentences are true, the semantic value is

.

The semantic value of a quantified term with an interpretation

and variable assigment

is determined by the semantic value of the embedded term or the truth value of the embedded sentence under the same interpretation but with various new versions of the variable assignment. We say that a variable assignment

is a *version* of variable assignment

with respect to variables

, ....,

if and only if

agrees with

on all variables except for

, ....,

. The assignments for

, ....,

can be the same as those in

or can be completely different.

The referent of a designator with term

as first argument and sentence

can be one of two things. Consider all versions

of

with respect to the free variables in

. If there is at least one version

that makes

true and the semantic value of

is the same in every

that makes

true, then the semantic value of the designator as a whole is that value. If there is more than one such value, the semantic value is

.

A set-forming term with the term

as first argument and the sentence

as second argument denotes the set of objects in the universe of discourse with the following properties. (1) The object must be the semantic value of

for some version

of

that makes

true. (2) The object must be *bounded*. A
term is *bounded* if and only if it satisfies the interpretation of the `bounded` relation. See the chapter on sets for the axioms characterizing this
relation.

A function-forming term denotes the set of tuples of bounded objects corresponding to the function that maps every tuple of objects matching the first argument of the term into the semantic value of the second argument.

If the argument list of the function-forming term terminates in a sequence variable, the semantic value of the term is the union of the infinite series of sets of tuples corresponding to (1) the same term in which all occurrences of the sequence variable are dropped, (2) the same term in which all occurrences of the sequence variable are replaced by a single individual variable, (3) the same term in which all occurrences of the sequence variable are replaced by two individual variables, etc.

A relation-forming term denotes the set of all tuples of bounded objects that satisfy the embedded sentence.

Wed Dec 7 13:23:42 PST 1994