%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\font\eightrm=cmr10 scaled 800
\font\twelverm=cmr10 scaled \magstep1
\font\twelvebf=cmbx10 scaled \magstep1
\font\fourteenrm=cmr10 scaled \magstep2
\font\fourteenbf=cmbx10 scaled \magstep2
\def\chapter#1#2{\bigskip
\sectioncount=0
\equationcount=0
\hfil{\twelvebf Chapter #1}
\medskip
\hfil{\fourteenbf #2}
\bigskip
\def\thechapter{#1}}
\def\appendix#1#2{\bigskip
\sectioncount=0
\equationcount=0
\hfil{\twelvebf Appendix #1}
\medskip
\hfil{\fourteenbf #2}
\bigskip
\def\thechapter{#1}}
\def\thechapter{1}
\countdef\sectioncount=11
\countdef\subsectioncount=13
\countdef\subsubsectioncount=15
\sectioncount=0
\subsectioncount=0
\subsubsectioncount=0
\def\section#1{\advance\sectioncount by 1\subsectioncount=1
\bigskip\noindent{\bf\S\thechapter.\the\sectioncount\ #1}\par
\nobreak\medskip}
\def\subsection#1{\advance\subsectioncount by 1
\bigskip\noindent{\bf#1}\par\nobreak\medskip}
\def\nosection#1{\bigskip\noindent{\bf#1}\par\nobreak\medskip}
\def\sect#1{\advance\sectioncount by1\subsectioncount=0
\nobreak\bigskip\noindent{\bf\the\sectioncount. #1}\par\medskip}
\def\subsect#1{\advance\subsectioncount by 1\subsubsectioncount=0
\bigskip\noindent{\bf\the\sectioncount.\the\subsectioncount\ #1}\par
\nobreak\medskip}
\def\subsubsect#1{\advance\subsubsectioncount by 1
\bigskip\noindent
{\bf\the\sectioncount.\the\subsectioncount.\the\subsubsectioncount\ #1}\par
\nobreak\medskip}
\def\nosect#1{\bigskip\noindent{\bf#1}\par\nobreak\medskip}
\def\heading#1{\bigskip\noindent{\bf#1}\par\medskip}
\countdef\equationcount=17
\equationcount=0
\def\equation{\global\advance\equationcount by 1
\thechapter.\the\equationcount}
\countdef\count=19
\count=0
\def\theorem#1#2{\medskip\noindent{\bf#1:\ }{\it#2}\par\medskip}
\def\proof#1{\medskip\noindent{\bf Proof:\ }#1\par\medskip}
\def\uncatcodespecials{\def\do##1{\catcode`##1=12}\dospecials}
\def\setupverbatim{\tt\def\par{\leavevmode\endgraf}\catcode`\`=\active
\obeylines\uncatcodespecials\obeyspaces}
{\catcode`\`=\active \gdef`{\relax\lq}}
{\obeyspaces\global\let =\ }{\obeylines\global\let^^M=\par}
\def\beginverbatim{\par\begingroup\setupverbatim\doverbatim}
{\catcode`|=0 \catcode`\\=12
|obeylines|gdef|doverbatim^^M#1\endverbatim{#1|endgroup}}
\def\verbatim{\begingroup\setupverbatim\doverb}
\def\doverb#1{\def\next##1#1{##1\endgroup}\next}
\def\start{\ }
\def\bibitem#1#2{\medskip\noindent}
\def\cite#1{[#1]}
\def\date{\the\day\ \ifcase\month\or January\or February\or March\or
April \or May\or June\or July\or August
\or September\or October\or November\or December\fi\ \the\year}
\def\defconcept#1#2{\medskip\noindent{\tt #1} - }
\magnification=\magstep1
\font\bigrm=cmr10 scaled \magstep1
\def\\{\char'134}
\def\^{\char'136}
\def\_{\char'137}
\def\~{\char'176}
\def\kif#1{\hbox{\tt #1}}
\def\non#1{\langle #1\rangle}
\def\or{\hbox{\tt\ }\;|\;\hbox{\tt\ }}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
Intuitively, the semantics of KIF is very simple. Unfortunately, the formal
details are quite complex. Consequently, we proceed gradually in our
presentation. In this chapter, we introduce the basic notions underlying the
semantics of KIF (in particular, the notions of conceptualization,
interpretation, variable assignment, semantic value, truth value, and logical
entailment).
The basis for KIF semantics is a correlation between the terms and sentences of the
language and a conceptualization of the world. Every term denotes an object in
the universe of discourse associated with the conceptualization, and every
sentence is either true or false.
When we encode knowledge in KIF, we select constants on the basis of our
understanding of their meanings. In some cases (e.g. the basic constants of the
language), these meanings are fixed in the definition of the language. In other
cases (i.e. the non-basic constants), the meanings can vary from one user to another.
Given exact meanings for the constants of the language (whether they are the
meanings in the definition of the language or our own concoctions), the
semantics of KIF tells us the meaning of its complex expressions. We can
unambiguously determine the referent of any term, and we can unambiguously
determine the truth or falsity of any sentence.
Unfortunately, few of us have complete knowledge about the world. In keeping with
traditional logical semantics, this is equivalent to not knowing the exact referent
for every constant in the language. In such situations, we write sentences that
reflect all of the meanings consistent with whatever knowledge we have. In such
situations, the semantics of the language cannot pick out exact meanings for all
expressions in the language, but it does place constraints on the meanings of complex
expressions.
And, of course, the meanings we ascribe to non-basic constants may differ from
those ascribed by others. However, we can convey our meanings to others by
writing sentences to constrain those meanings in accordance with our usage. By
writing more and more sentences, the set of possible referents for our constants is
decreased.
In the remainder of this chapter, we provide precise definitions for the ideas
just introduced. We start off with a definition for the notion of
conceptualization. Using this concept, we introduce the notion of {\it
interpretation} of constants, and we introduce the related notion of {\it
variable assignment}. We then show how these concepts are used in defining the
{\it semantic value} of terms and the {\it truth value} of sentences. Finally,
we define {\it logical entailment}, which eliminates the dependence of meaning
on the interpretation of non-basic constants. We also give a partial
description of the semantics of definitions. (A full treatment is given in
the chapter on definitions.)
\section{Conceptualization}
The formalization of knowledge in KIF, as in any declarative representation,
requires a {\it conceptualization} of the world in terms of objects,
functions, and relations.
A {\it universe of discourse} is the set of all objects presumed or
hypothesized to exist in the world. The notion of {\it object} used here is
quite broad. Objects can be concrete (e.g. a specific carbon atom, Confucius,
the Sun) or abstract (e.g. the number 2, the set of all integers, the concept
of justice). Objects can be primitive or composite (e.g. a circuit that
consists of many subcircuits). Objects can even be fictional (e.g. a unicorn,
Sherlock Holmes).
Different users of a declarative representation language, like KIF, are likely
to have different universes of discourse. KIF is {\it conceptually
promiscuous} in that it does {\it not} require every user to share the same
universe of discourse. On the other hand, KIF is {\it conceptually grounded}
in that every universe of discourse {\it is} required to include certain {\it
basic} objects.
The following basic objects must occur in every universe of discourse.
\medskip
\item{$\bullet$} Characters.
\medskip
\item{$\bullet$} Words. Yes, the words of KIF are themselves objects in the
universe of discourse, along with the things they denote.
\medskip
\item{$\bullet$} All finite lists of objects in the universe of discourse.
\medskip
\item{$\bullet$} $\bot$ (pronounced ``bottom'') -- a distinguished object that
occurs as the value of various functions when applied to arguments for which
the functions make no sense.
\medskip
Remember, however, that to these basic elements, the user can
add whatever {\it non-basic} objects seem useful.
A function is one kind of interrelationship among objects. For every finite
sequence of objects (called the {\it arguments}), a {\it function} associates a
unique object (called the {\it value}). More formally, a function is defined as
a set of finite lists of objects, one for each combination of possible
arguments. In each list, the initial elements are the arguments, and the final
element is the value. For example, the $1+$ function contains the list
$\langle 2,3\rangle$, indicating that integer successor of $2$ is $3$.
A relation is another kind of interrelationship among objects in the universe
of discourse. More formally, a {\it relation} is an arbitrary set of finite
lists of objects (of possibly varying lengths). Each list is a selection of
objects that jointly satisfy the relation. For example, the $<$ relation on
numbers contains the list $\langle 2,3\rangle$, indicating that $2$ is
less than $3$.
Note that both functions and relations are defined as sets of lists. In fact,
every function is a relation. However, not every relation is a function. In a
function, there cannot be two lists that disagree on only the last element.
This would be tantamount to the function having two values for one combination
of arguments. By contrast, in a relation, there can be any number of lists
that agree on all but the last element. For example, the list $\langle
2,3\rangle$ is a member of the $1+$ function, and there is no other list of
length 2 with $2$ as its first argument, i.e. there is only one successor for
$2$. By contrast, the $<$ relation contains the lists $\langle 2,3\rangle$,
$\langle 2,4\rangle$, and so forth, indicating that $2$ is less than $3$, $4$,
and so forth.
Many mathematicians require that functions and relations have fixed arity, i.e
they require that all of the lists comprising a function or relation have the
same length. The definitions here allow for functions and relations with
variable arity, i.e. it is perfectly acceptable for a function or a relation to
contain lists of different lengths. For example, the $+$ function contains
the lists $\langle 1,1,2\rangle$ and $\langle 1,1,1,3\rangle$, reflecting the
fact that the sum of $1$ and $1$ is $2$ and the fact that the sum of $1$ and
$1$ and $1$ is $3$. Similarly, the relation $<$ contains the lists $\langle
1,2\rangle$ and $\langle 1,2,3\rangle$, reflecting the fact that $1$ is less
than $2$ and the fact that $1$ is less than $2$ and $2$ is less than $3$.
This flexibility is not essential, but it is extremely convenient and poses no
significant theoretical problems.
\section{Interpretation}
An {\it interpretation} is a function $i$ that associates the constants of
KIF with the elements of a conceptualization. In order to be an interpretation, a
function must satisfy the following two properties.
First, the function must map constants into concepts of the appropriate type. It
must map object constants into objects in the universe of discourse. It must map
function constants into functions on the universe of discourse. It must map relation
constants into relations on the universe of discourse. Notice that we allow for
functions and relations of variable, finite arity. It must map logical constants into
one of the boolean values $true$ or $false$ (which may or may not be members of the
universe of discourse).
\medskip
\item{1.} If $\sigma$ is an object constant, then $i(\sigma)\in O$.
\item{2.} If $\sigma$ is a function constant, then
$i(\sigma):O^*\longrightarrow O$.
\item{3.} If $\sigma$ is a relation constant, then $i(\sigma)\subseteq O^*$.
\item{3.} If $\sigma$ is a logical constant, then $i(\sigma)\in\{true,false\}$.
\medskip
Second, $i$ must ``satisfy'' (in the sense defined below) the numbered axioms given in
the remaining chapters of this document.
Note that, even with these restrictions, KIF is only a ``partially interpreted''
language. Although the interpretations of some constants are constrained in the
definition of the language, the meanings of other constants are left open (i.e. left
to the imaginations of the language users).
\section{Variable Assignment}
A {\it variable assignment} is a function that (1) maps individual variables
${\cal V}$ into objects in a universe of discourse $O$ and (2) maps sequence
variables ${\cal W}$ into finite sequences of objects.
The notion of a variable assignment is important in defining the meaning of
quantified terms and sentences and is discussed further below.
\section{Semantic Value}
Given an interpretation and a variable assignment, we can assign a {\it
semantic value} to every expression in the language. We formalize this as a function
$s_{iv}$ from the set ${\cal T}$ of terms into the set $O$ of objects in the universe of discourse.
$$s_{iv}:{\cal T}\longrightarrow O$$
If an expression is an individual variable $\nu$, the semantic value is the
object assigned to that variable by the given variable assignment.
$$s_{iv}(\nu)=v(\nu)$$
The semantic value of an object constant $\sigma$ is the object assigned to
that constant by the given interpretation.
$$s_{iv}(\sigma)=i(\sigma)$$
\section{Truth Value}
In a manner similar to that for terms, we define the {\it truth value} for
sentences in the language as a function $t_{iv}$ that maps sentences ${\cal S}$
into the truth values $true$ or $false$.
$$t_{iv}:{\cal S}\longrightarrow\{true,false\}$$
The truth value of a logical constant is the truth value assigned by the
corresponding interpretation.
$$t_{iv}(\lambda)=i(\lambda)$$
\section{Logical Entailment}
The definition of truth value relies on both an interpretation for the constants
of KIF and an assignment for its variables. In encoding knowledge, we often
have in mind a specific interpretation for the constants in our language, but we
want our variables to range over the universe of discourse (either existentially
or universally). In order to provide a notion of semantics that is independent of
the assignment of variables, we turn to the notion of satisfaction.
An interpretation $i$ {\it logically satisfies} a sentence $\phi$ if and only if
the truth value of the sentence is $true$ for all variable assignments. Whenever
this is the case, we say that $i$ is a {\it model} of $\phi$. Extending this
notion to sets of sentences, we say that an interpretation is a model of a set of
sentences if and only if it is a model of every sentence in the set of sentences.
Obviously, a variable assignment has no effect on the truth value of a
sentence without free variables (i.e. a ground sentence or one in which all
variables are bound). Consequently, if an interpretation satisfies such a sentence
for one variable assignment, it satisfies it for every variable assignment.
The occurrence of free variables in a sentence means that the sentence is true
for all assignments of the variables. For example, the sentence {\tt (p ?x)}
means that the relation denoted by {\tt p} is true for all objects in the
universe of discourse. In other words, the meaning of a sentence with free
variables is the same as the meaning of a universally quantified sentence in
which all of the free variables are boundby the universal quantifier. In KIF, we use
this fact to sanction the dropping of prefix universal quantifiers that do not occur
inside the scope of existential quantifiers. In other words, we are permitted to
write {\tt (=> (apple ?x) (red ?x))} in place of the more cumbersome {\tt
(forall (?x) (=> (apple ?x) (red ?x)))}.
Unfortunately, the notion of satisfaction is disturbing in that it is relative
to an interpretation. As a result, different individuals and different programs
with different interpretations may disagree on the truth of a sentence.
It is true that, as we add more sentences to a knowledge base, the set of
models generally decreases. The goal of knowledge encoding is to write enough
sentences so that unwanted interpretations are eliminated. Unfortunately, this
is not always possible. In the light of this fact, how are we to interpret the
expressions in such situations? The answer is to generalize over interpretations
as earlier we generalized over variable assignments.
If $\Delta$ is a set of sentences, we say that $\Delta$ {\it logically entails} a
sentence $\phi$ if and only every model of $\Delta$ is also a model of $\phi$.
With this notion, we can rephrase the goal of knowledge representation as
follows. It is to encode enough sentences so that every conclusion we desire
is logically entailed by our set of sentences. It is a sad fact
that this is not always possible, but it is the ideal toward which we strive.
\section{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 {\it content} of the definition.
The rules for determining the content of a definition are slightly 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 {\tt defobject} operator is used to define objects. The two simplest
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.
\bigskip
\centerline{\vbox{\halign{\strut#\hfil\quad&\quad#\hfil\cr
\hfil Definition&\hfil Defining Axiom\cr
\noalign{\hrule}
{\tt (defobject $\sigma$ := $\tau$)}&{\tt (= $\sigma$ $\tau$)}\cr
&\cr
{\tt (defobject $\sigma$ $\phi_1$ ... $\phi_n$)}&{\tt (and $\phi_1$ ...
$\phi_n$)}\cr}}}
\bigskip
The {\tt 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 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.
\bigskip
\centerline{\vbox{\halign{\strut#\hfil\quad&\quad#\hfil\cr
\hfil Definition&\hfil Defining Axiom\cr
\noalign{\hrule}
{\tt (deffunction $\pi$ ($\nu_1$ ...$\nu_n$) := $\tau$)}&{\tt (= ($\pi$
$\nu_1$ ...$\nu_n$) $\tau$)}\cr
&\cr
{\tt (deffunction $\pi$ $\phi_1$ ... $\phi_n$)}&{\tt (and $\phi_1$
... $\phi_n$)}\cr}}}
\bigskip
The {\tt defrelation} operator is used to define relations. The two simplest
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.
\bigskip
\centerline{\vbox{\halign{\strut#\hfil\quad&\quad#\hfil\cr
\hfil Definition&\hfil Defining Axiom\cr
\noalign{\hrule}
{\tt (defrelation $\rho$ ($\nu_1$ ...$\nu_n$) := $\phi$)}&{\tt (<=> ($\rho$
$\nu_1$ ...$\nu_n$) $\phi$)}\cr
&\cr
{\tt (defrelation $\rho$ $\phi_1$ ... $\phi_n$)}&{\tt (and $\phi_1$ ...
$\phi_n$)}\cr}}}
\bigskip
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\vfill\eject
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{4}{Logical Expressions}
\section{Bottom}
The semantic value of the object constant {\tt bottom} is $\bot$.
$$s_{iv}(\hbox{\tt bottom})=\bot$$
\section{Functional Terms}
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.
$$s_{iv}(\hbox{\tt ($\pi$
$\tau_1$...$\tau_n$)})=i(\pi)[s_{iv}(\tau_1),...,s_{iv}(\tau_n)]$$
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.)
$$s_{iv}(\hbox{\tt ($\pi$ $\tau_1$...$\tau_n$ $\omega$)})=
i(\pi)[s_{iv}(\tau_1),...,s_{iv}(\tau_n)|s_{iv}(\omega)]$$
\section{Conditional Terms}
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 $true$, 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).
$$s_{iv}(\hbox{\tt (if $\phi$ $\tau_1$ $\tau_2$)})=\cases{
s_{iv}(\tau_1)&$t_{iv}(\phi)=true$\cr
s_{iv}(\tau_2)&otherwise\cr}$$
If a simple conditional has only one embedded term and the truth value of the embedded
sentence is $true$, then the semantic value of the term is the semantic value of the
embedded term. Otherwise, the value is $\bot$.
$$s_{iv}(\hbox{\tt (if $\phi$ $\tau_1$)})=\cases{
s_{iv}(\tau_1)&$t_{iv}(\phi)=true$\cr
\bot&otherwise\cr}$$
The semantic value of a complex conditional is the semantic value of the {\it
first} term for which the truth value of the corresponding sentence is $true$.
If none of the sentences are true, the semantic value is $\bot$.
$$s_{iv}(\hbox{\tt (cond ($\phi_1$ $\tau_1$) ... ($\phi_n$ $\tau_n$))})=\cases{
s_{iv}(\tau_1)&$t_{iv}(\phi_1)=true$\cr
\;\;\;...&\hfil...\hfil\cr
s_{iv}(\tau_2)&$t_{iv}(\phi_n)=true$\cr
\bot&otherwise\cr}$$
\section{True and False}
The truth value of {\tt true} is $true$, and the truth value of {\tt false}
is $false$.
$$\eqalign{s_{iv}(\hbox{\tt true})&=true\cr
\cr
s_{iv}(\hbox{\tt false})&=false\cr}$$
\section{Equations and Inequalities}
An equation is true if and only if the terms in the equation refer to the same object
in the universe of discourse.
$$t_{iv}(\hbox{\tt (= $\tau_1$ $\tau_2$)})=\cases{
true&$s_{iv}(\tau_1)=s_{iv}(\tau_2)$\cr
false&otherwise\cr}$$
An inequality is true if and only if the terms in the equation refer to distinct
objects in the universe of discourse.
$$t_{iv}(\hbox{\tt (/= $\tau_1$ $\tau_2$)})=\cases{
false&$s_{iv}(\tau_1)=s_{iv}(\tau_2)$\cr
true&otherwise\cr}$$
\section{Relational Sentences}
The truth value of a simple relational sentence without a terminating sequence
variable is $true$ if and only if the relation denoted by the relation constant
in the sentence is true of the objects denoted by the arguments. Equivalently,
viewing a relation as a set of tuples, we say that the truth value of a
relational sentence is $true$ if and only if the tuple of objects formed from
the values of the arguments is a member of the set of tuples denoted by the
relation constant.
$$t_{iv}(\hbox{\tt ($\rho$ $\tau_1$ ... $\tau_n$)})=\cases{
true&$\langle s_{iv}(\tau_1),...,s_{iv}(\tau_n)\rangle\in i(\rho)$\cr
false&otherwise\cr}$$
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. Remember that the vertical bar $|$ means that the objects in the sequence following the bar are appended to the sequence of elements before the bar.
$$t_{iv}(\hbox{\tt ($\rho$ $\tau_1$ ... $\tau_n$ $\omega$)})=\cases{
true&$\langle s_{iv}(\tau_1),...,s_{iv}(\tau_n)|s_{iv}(\omega)\rangle\in
i(\rho)$\cr false&otherwise\cr}$$
\section{Logical Sentences}
The truth value of a negation is $true$ if and only if the truth value of
the negated sentence is $false$.
$$t_{iv}(\hbox{\tt (not $\phi$)})=\cases{
true&$t_{iv}(\phi)=false$\cr
false&otherwise\cr}$$
The truth value of a conjunction is $true$ if and only if the truth value of
every conjunct is $true$.
$$t_{iv}(\hbox{\tt (and $\phi_1$ ... $\phi_n$)})=\cases{
true&$t_{iv}(\phi_j)=true$ for all $j$ $1\leq j\leq n$\cr
false&otherwise\cr}$$
The truth value of a disjunction is $true$ if and only if the truth value of at
least one of the disjuncts is $true$.
$$t_{iv}(\hbox{\tt (or $\phi_1$ ... $\phi_n$)})=\cases{
true&$t_{iv}(\phi_j)=true$ for some $j$ $1\leq j\leq n$\cr
false&otherwise\cr}$$
If the truth value of every antecedent in an implication is $true$, then the
the truth value of the implication as a whole is $true$ if and only if the truth
value of 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.
$$t_{iv}(\hbox{\tt (=> $\phi_1$ ... $\phi_n$ $\phi$)})=\cases{
true&for some $j$ $t_{iv}(\phi_j)=false$ or
$t_{iv}(\phi)=true$\cr
false&otherwise\cr}$$
A reverse implication is just an implication with the consequent and antecedents
reversed.
$$t_{iv}(\hbox{\tt (<= $\phi$ $\phi_1$ ... $\phi_n$)})=\cases{
true&$t_{iv}(\phi)=true$ or for some $j$ $t_{iv}(\phi_j)=false$\cr
false&otherwise\cr}$$
The truth value of an equivalence is $true$ if and only if the embedded
sentences have the same truth value.
$$t_{iv}(\hbox{\tt (<=> $\phi_1$ $\phi_2$)})=\cases{
true&$t_{iv}(\phi_1)=t_{iv}(\phi_2)$\cr
false&otherwise\cr}$$
\section{Quantified Sentences}
The semantic value of a quantified sentence with an interpretation $i$ and
variable assigment $v$ is determined by the truth value of the embedded
sentence under the same interpretation but with various new versions of the
variable assignment. Recall that a variable assignment $v'$ is a {\it version}
of variable assignment $v$ with respect to variables $\nu_1$, ...., $\nu_n$ if
and only if $v'$ agrees with $v$ on all variables except for $\nu_1$, ....,
$\nu_n$. The assignments for $\nu_1$, ...., $\nu_n$ can be the same as those in
$v$ or can be completely different.
Given an interpretation $i$ and variable assignment $v$, the truth value of
a simple existentially quantified sentence (one in which the first argument is
a list of variables) is $true$ if and only if the truth value of the second
argument is $true$ for {\it some} version $v'$ of variable assignment $v$ with
respect to the variables in the first argument.
$$t_{iv}(\hbox{\tt (exists ($\nu_1$ ... $\nu_k$ $\omega$) $\phi$)})=\cases{
true&$\exists v'\;t_{iv'}(\phi)=true$\cr
false&otherwise\cr}$$
Given an interpretation $i$ and variable assignment $v$, the truth value of a
simple universally quantified sentence (onein which the first argument is
a list of variables) is $true$ if and only if the truth value of the second
argument of the sentence is $true$ for {\it every} version $v'$ of $v$ with
respect to variables in the first argument.
$$t_{iv}(\hbox{\tt (forall ($\nu_1$ ... $\nu_k$ $\omega$) $\phi$)})=\cases{
true&$\forall v'\;t_{iv'}(\phi)=true$\cr
false&otherwise\cr}$$
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 are examples of quantified sentences and their simplified equivalents.
\bigskip
{\tt (forall ((?x integer)) (number ?x))}\par
{\tt (forall (?x) (=> (integer ?x) (number ?x)))}\par
\bigskip
{\tt (exists ((?x integer)) (< ?x 0))}\par
{\tt (exists (?x) (and (integer ?x) (< ?x 0)))}\par
\bigskip
{\tt (forall ((?x in integers)) (number ?x))}\par
{\tt (forall (?x) (=> (member ?x integers) (number ?x)))}\par
\bigskip
{\tt (exists ((?x in integers)) (< ?x 0))}\par
{\tt (exists (?x) (and (member ?x integers) (< ?x 0)))}\par
\bigskip
{\tt (forall ((?x in (f ?y)) (?y in cars)) (p ?x ?y))}\par
{\tt (forall (?x ?z) (=> (member ?x (f ?y)) (member ?z cars) (p ?x ?z)))}
\bigskip
\bye
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%