%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Excerpts from my macro file
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\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

\countdef\sectioncount=11
\countdef\subsectioncount=13
\countdef\subsubsectioncount=15
\sectioncount=0
\subsectioncount=0
\subsubsectioncount=0

\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\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\bibitem#1#2{\medskip\noindent}
\def\cite#1{[#1]}

\def\begconcept{\bigskip\hrule\par\nobreak
\noindent\vrule height3pt\hfill\vrule height3pt\par\nobreak}

\def\midconcept{\nobreak\medskip\hrule\medskip\par}

\def\defconcept#1#2{\noindent{\tt #1}\hfill{\it #2}\par\nobreak}

\def\difconcept#1#2{\noindent{\tt #1}\hfill{\it #2}\par\medskip}

\def\endconcept{\nobreak\noindent\vrule height3pt\hfill\vrule height3pt\par
\nobreak\hrule\bigskip}

\countdef\eqcount=17
\eqcount=1
\def\eqn{\the\eqcount\advance\eqcount by1}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Text starts here
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\magnification=\magstep1
\font\bigrm=cmr10 scaled \magstep1
\noindent Logic Group \hfill First Draft May 1990\break
Report Logic-90-4 \hfill Current Version March 1991\par
\vfill
\centerline{\bigrm Knowledge Interchange Format}
\centerline{\bigrm Version 2.2}
\centerline{\bigrm Reference Manual}
\vskip5mm
\centerline{\it by}
\vskip5mm
\centerline{\bigrm Michael R. Genesereth}
\centerline{\bigrm Richard Fikes}
\vskip5mm
\centerline{\it in collaboration with}
\vskip5mm
\centerline{\bigrm\vbox{\halign{#\hfil\cr
Danny Bobrow\cr
Piero Bonissone\cr
Ron Brachman\cr
Ramanathan Guha\cr
Reed Letsinger\cr
Vladimir Lifschitz\cr}}
\quad\vbox{\halign{#\hfil\cr
Bob MacGregor\cr
John McCarthy\cr
Peter Norvig\cr
Ramesh Patil\cr
Len Schubert\cr}}}
\vfill

This manual is the "living document" of the Interlingua Working Group of
the DARPA Knowledge Represenation Standards Effort.  As such, it
represents work in progress toward a proposal for a standard knowledge
interchange format to be used in support of the creation, sharing, and
reuse of large knowledge bases.

\vfill
\centerline{Computer Science Department}
\centerline{Stanford University}
\centerline{Stanford, California 94305}
\eject

Abstract: {\it Knowledge Interchange Format} (KIF) is a computer-oriented
language for the interchange of knowledge among disparate programs.  It has
declarative semantics (i.e. the meaning of expressions in the representation can
be understood without appeal to an interpreter for manipulating those
expressions); it is logically comprehensive (i.e. it provides for the
expression of arbitrary sentences in the first-order predicate calculus);
and it is self-descriptive (i.e. it provides for the representation of
knowledge about the representation of knowledge).  

\vfill\eject

\sect{Introduction}

{\it Knowledge Interchange Format} (KIF) is a formal language for the interchange
of knowledge among disparate computer programs (written by different programmers,
at different times, in different languages, and so forth). 

KIF is {\it not} intended as a primary language for interaction with human users
(though it can be used for this purpose).  Different programs can interact with
their users in whatever forms are most appropriate to their applications (for
example frames, graphs, charts, tables, diagrams, natural language, and so forth).

KIF is also {\it not} a standard for the internal representation of knowledge {\it
within} computer programs or within closely related sets of programs (though it
can be used for this purpose as well).  Typically, when a program reads a database
in KIF, it converts the data into its own internal form (specialized pointer
structures, arrays, etc.).  All computation is done using these internal forms. 
When the program needs to communicate with another program, it maps its internal
data structures into KIF.

The purpose of KIF is roughly analogous to that of Postscript.  Postscript
is commonly used by text and graphics formatting programs in communicating
information about documents to printers.  Although it is not as efficient as a
specialized representation for documents and not as perspicuous as a specialized
wysiwyg display, Postscript is a programmer-readable representation that
facilitates the independent development of formatting programs and printers. 
While KIF is not as efficient as a specialized representation for knowledge nor
as perspicuous as a specialized display (when printed in its list form), it too
is a programmer-readable standard and thereby facilitates the independent
development of knowledge-manipulation programs.

The definition of KIF is highly detailed.  Some of these details are essential;
others are arbitrary.   The following general features are essential in the
definition of KIF.

\medskip

\item{1.} The language has declarative semantics.  It is possible to
understand the meaning of expressions in the language without appeal to an
interpreter for manipulating those expressions.  In this way, KIF differs from
other languages that are based on specific interpreters, such as Emycin
and Prolog.

\item{2.} The language is logically comprehensive -- it provides for the
expression of arbitrary sentences in predicate calculus. In this way,
it differs from relational database languages (many of which are confined to
ground atomic sentences) and Prolog-like languages (that are confined to Horn
clauses).

\item{3.} The language provides for the representation of knowledge about the
representation of knowledge.  This allows us to make all knowledge
representation decisions explicit and permits us to introduce new knowledge
representation constructs without changing the language standard.

\medskip

In addition to these hard criteria, KIF is designed to maximize in a joint fashion
the following somewhat softer measures as well (to the extent possible while
satisfying the preceding criteria).

\medskip

\item{1.} Translatability.  A central operational requirement for KIF is
that it enable practical means of translating declarative knowledge
bases to and from typical knowledge representation languages.

\item{2.} Readability.  Although KIF is not intended primarily as a
language for interaction with humans, human readability will facilitate
its use to describe representation language semantics, its use as a
publication language for example knowledge bases, human assistance with
translation problems, etc.

\item{3.} Useability as a representation language.  Although KIF is not
intended for use within programs as a representation or communication
language, it {\it can} be used for that purpose if so desired.

\medskip

This document supplies full technical details of KIF.  Section~2 presents the
formal syntax of the language.  Section~3 discusses conceptualizations of the
world.  Section~4 outlines the semantics of the language.  The remaining
section introduce the semantics of the basic vocabulary.  The appendix lists
words that are reserved for possible future inclusion in the standard.

{\it NB: This document is not yet complete.  Areas where open questions remain
are annotated by comments in italics.  Our job in aswering these open
questions (as opposed to our job in approving the existing portion of the
standard) is not so much to change the Roman text as to eliminate the italics.}

\vfill\eject

\sect{Syntax}

Like many computer-based languages, KIF has two varieties.  In {\it linear} KIF,
all expressions are strings of ASCII characters and, as such, are suitable for
storage on serial devices (such as magnetic disks) and for transmission
on serial media (such as phone lines).  In {\it structured} KIF, the legal
``expressions'' of the language are Lisp-like lists (pointer structures of a
sort).  Structured KIF is of special use in standardizing communication between
programs operating in the same address space.  

Fortunately, there is a simple correspondence between the two varieties of KIF. 
For every character string, there is exactly one corresponding list structure;
and, for every list structure, there is exactly one corresponding character
string (once all unnecessary white space is eliminated). 

In what follows, we first define the mapping between the linear and structured
forms of the language; and, thereafter, we deal exclusively with the structured
form.

\subsect{Linear KIF}

The alphabet of linear KIF consists of the 128 characters in the ASCII character
set.  Some of these characters have standard print representations; others do
not.  The characters with standard print representations (93 of the 128) are shown
below.

\medskip
\beginverbatim
        A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
        a b c d e f g h i j k l m n o p q r s t u v w x y z
        0 1 2 3 4 5 6 7 8 9 ( ) [ ] { } < > 
        = + - * / \ & ^ ~ ' ` " _ @ # $ % : ; , . ! ?
\endverbatim
\medskip

KIF originated in a Lisp application and inherits its syntax from Lisp.  This
choice makes it especially easy for Lisp programmers to read sentences written in
the language, though it may be somewhat awkward for non-Lisp programmers. 
More importantly, Lisp syntax makes the process of parsing expressions
quite simple. 

The relationship between linear KIF and structured KIF is most easily specified
by appeal to the Common Lisp reader.  In particular, a string of ascii characters
forms a legal sentence in linear KIF if and only if (1) it is acceptable to the
Common Lisp reader (as defined in Steele's book) and (2) the structure produced
by the Common Lisp reader is a legal sentence of structured KIF (as defined
below).

\subsect{Structured KIF}

In discussing KIF expressions in what follows, we assume that standard Lisp
parsing has already taken place; and therefore, we talk about {\it atoms} and
{\it lists}, rather than individual characters.

The basic building blocks of KIF are Lisp atoms.  This includes symbols,
numbers, strings, vectors, arrays, and so forth. In KIF, the set of Lisp atoms
is divided into the categories listed in Table~I.  This categorization is
disjoint and exhaustive.  Every atom is a member of one and only one category. 
(The categories defined here are used again in the grammatical rules of
subsequent tables.)

\pageinsert
\vfill
\bgroup
\parskip=10pt
\medskip
{\tt <indvar> ::= {\it a symbol beginning with the character} \$}

{\tt <seqvar> ::= {\it a symbol beginning with the character} @}

{\tt <termop> ::= if | cond | value | setof | quote}

{\tt <sentop> ::= not | and | or | => | <= | <=> |}
{\tt \ \ \ \ \ \ \ \ \ \ \ \ \ forall | exists | holds |}

{\tt \ \ \ \ \ \ \ \ \ \ \ \ \ defobject | defunction | defprimrelation |
defrelation}

{\tt <objconst> ::= {\it a constant denoting an object}}

{\tt <funconst> ::= {\it a constant denoting a function}}

{\tt <relconst> ::= {\it a constant denoting a relation}}

{\tt <logconst> ::= {\it a constant denoting a truth value}}
\medskip
\egroup
\vfill
\centerline{Table~I - Categorization of atoms in KIF}
\endinsert

A {\it variable} is a symbol in which the first category is {\tt \$} or {\tt @}. 
A variable that begins with {\tt \$} is called an {\it individual variable}.  A
variable that begins with an {\tt @} is called a {\it sequence variable}. 
Individual variables are used in quantifying over objects.  Sequence
variables are used in quantifying over sequences of objects.

{\it Operators} are used in forming complex exprsssions in which sentences occur
as components.  There are two types of operators in KIF -- {\it term operators}
and {\it sentence operators}.  Term operators are used in forming complex terms in
which sentences occur as components.  Sentence operators are used in forming
sentences. The following symbols are sentence operators in KIF.

A {\it constant} is any atom that is neither a variable nor an operator.  There
are four categories of constants in KIF -- object constants, function constants,
relation constants, and logical constants.  {\it Object constants} are used to
denote objects in the world.  {\it Function constants} denote functions on
those objects.  {\it Relation constants} denote relations.  {\it Logical
constants} express atomic conditions about the world and are either true or
false.

Some constants are {\it basic} in that their type and meaning are fixed in the
definition of KIF.  All other constants are {\it non-basic} in that the language
user gets to choose the type and the meaning.  All numbers, characters, and strings
are basic constants in KIF; the remaining basic constants are described in
the remaining sections of this document.

KIF is unusual among logical languages in there is no way of determining
the category of a non-basic constant (i.e. whether it is an object, function,
relation, or logical constant) from its inherent properties (i.e. its spelling). 
The user selects the category of every non-basic constant for himself.  The user
need not declare his choice explicitly.  However, the category of a constant
determines how it can be used in forming special expressions, and its category
{\it can} be determined from this use.   Consequently, once a constant is used in
a particular way, its category becomes fixed.  

While every Lisp atom is a legal expression in KIF, this is not true of every
list.  There are two types of legal list expressions in the language -- {\it
terms} and {\it sentences}.  Terms are used to denote objects in the world being
described, and sentences are used to express facts about the world.

The modified BNF in Table~II defines the set of legal terms in the
format.  There are eight types of terms -- individual variables, object
constants, function constants, relation constants, functional expressions,
logical terms, quantified terms, and quotations.  {\it Individual variables},
{\it object constants}, function constants, and relation constants were discused
earlier.  A {\it functional term} consists of a function constant and an
arbitrary number of terms, terminated by an optional sequence variable.  {\it
Logical terms} involve the {\tt if} and {\tt cond} operators.  (Note that a
logical term involving {\tt cond} differs in syntax from its counterpart in
Lisp.)  {\it Quantified terms} involve the {\tt setof} operator, an arbitrary
term, and an arbitrary sentence.  {\it Quotations} involve the operator {\tt
quote} and an arbitrary list expression.  (Note that the embedded expression can
be an arbitrary list structure; it need not be a legal expression in KIF.)
 
\pageinsert
\vfill
\beginverbatim

<term> ::= <indvar>|<objconst>|<funconst>|<relconst>|
           <funterm>|<logterm>|<quanterm>|<quotation>

<funterm> ::= (<funconst> <term>*)|
              (<funconst> <term>* <seqvar>)|
              (value <term> <term>*)|
              (value <term> <term>* <seqvar>)

<logterm> ::= (if <sentence> <term> <term>)|
              (cond <sentence> <term> ... <sentence> <term>)

<quanterm> ::= (setof <term> <sentence>)

<quotation> ::= (quote <listexpr>)

<listexpr> ::= <atom>|(<listexpr>*)

<atom> ::= <indvar>|<seqvar>|<termop>|<sentop>
           <objconst>|<funconst>|<relconst>|<logconst>
\endverbatim
\vfill
\centerline{Table~II - Legal terms in KIF}
\endinsert

The modified BNF in Table~III defines the set of legal sentences in KIF.  There
are five types of sentences.  We have already mentioned logical constants.  A
{\it relational sentence} consists of a relation constant and an arbitrary number
of terms, terminated by an optional sequence variable.  The syntax of {\it logical
sentences} depends on the logical operator involved.  There are two types of
quantified sentences -- a {\it universally quantified sentence} is signalled by the
use of the {\tt forall} operator, and an {\it existentially quantified sentence} is
signalled by the use of the {\tt exists} operator.  There are four kinds of
{\it definitional sentences} -- object, function, primitive relation, and
relation definitions.

\pageinsert
\vfill
\beginverbatim
<sentence> ::= <logconst>|<relsent>|<logsent>|<quantsent>|<defsent>

<relsent> ::= (<relconst> <term>*)|
              (<relconst> <term>* <seqvar>)|
              (holds <term> <term>*)|
              (holds <term> <term>*)

<logsent> ::= (not <sentence>)|
              (and <sentence>*)|
              (or <sentence>*)|
              (=> <sentence>* <sentence>)|
              (<= <sentence> <sentence>*)|
              (<=> <sentence> <sentence>)

<quantsent> ::= (forall <term> <sentence>)|
                (exists <term> <sentence>)

<defsent> ::= (defobject <objconst> <sentence>*)|
     (defunction <funconst> (<indvar>*) <term>)|
     (defunction <funconst> (<indvar>* <seqvar>) <term>)|
     (defrelation <relconst> (<indvar>*) <sentence>*)|
     (defrelation <relconst> (<indvar>* <seqvar>) <sentence>*)|
     (defprimrelation <relconst> (<indvar>*) <sentence>*)
     (defprimrelation <relconst> (<indvar>* <seqvar>) <sentence>*)
\endverbatim
\vfill
\centerline{Table~III - Legal sentences in KIF}
\endinsert

\vfill\eject

\sect{Conceptualization}

The formalization of knowledge in KIF, as in any declarative representation,
requires a {\it conceptualization} of the world.  This includes
the objects presumed or hypothesized to exist in the world, functions
on those objects, and relations among them.  The set of all objects, functions,
and relations about which knowledge is being expressed in a database is called
the {\it universe of discourse}.

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 circuits that consists of many subcircuits).  Objects can
even be fictional (e.g. a unicorn, Sherlock Holmes).

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}).  {\it Formal definition as a set of
tuples.}

A  relation is another kind of interrelationship among objects in the universe
of discourse.  Formally, we define a {\it relation} to be an arbitrary set of
tuples of objects.  

Different users of a declarative representation language are
likely to have different conceptualizations of the world.  KIF is {\it
conceptually promiscuous} in that it does {\it not} require every user to share the
same conceptualization of the world.  On the other hand, KIF is {\it conceptually
grounded} in that every  conceptualization {\it is} required to contain certain
{\it basic} objects, functions, and relations.  The grounding is only partial,
however; to these basic elements, the user can add whatever {\it non-basic}
objects, functions, and relations he finds useful.

All list expressions (i.e. atoms, lists of atoms, lists of atoms and lists, and
so forth) are basic objects.  (Yes, these expressions are themselves objects
in the universe of discourse.)

\vfill\eject

\sect{Semantics}

Intuitively, the semantics of KIF is very simple.  Unfortunately, the formal
details are quite complex.  Consequently, we proceed gradually in our
presentation.  In this section, we introduce the basic definitions underlying the
semantics of KIF (in particular, the notions of interpretation, variable
assignment, semantic value, truth value, satisfaction, and various different
types of entailment).  In each of the following sections, we fill in the details
for a different subset of the language.  Within each section, we give a formal
account of the semantics of the expressions covered by that section.  In some
cases, we introduce the formal account with an informal introduction to help
elucidate the formal details. 

The basis for KIF semantics is a correlation between the expressions 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 atoms 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), we use words in our own ways.  

Given exact meanings for the words 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. 

Of course, we often do not have complete knowledge about the world we want to
describe.  In keeping with traditional logical semantics, this is equivalent to
not knowing the exact referent for every word 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 does place
constraints on the meanings of complex expressions.

And, of course, the meanings we ascribe to non-basic words 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 words is decreased.

In the remainder of this section, we provide sharp definitions for the ideas just
introduced.  We start off with a definition for the {\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.  We then generalize the definition
of truth value to that of {\it satisfaction} and thereby eliminate the dependence
of meaning on variable assignment.  Finally, we introduce several different
approaches to {\it entailment}, which eliminates the dependence of meaning on
interpretation of non-basic constants.  All of the definitions are given here in
their entirety, except for the details of semantic value and truth value
associated with specific basic constants and operators of KIF.  These details form
the substance of the remaining sections of this document.

\subsect{Interpretation}

An {\it interpretation} is a function $i$ that associates the constants of KIF
with the elements of a universe of discourse $O$.  In order to be an
interpretation, a function must satisfy the following three properties.

First of all, $i$ must map every constant into an element of the universe of
discourse.  (Yes, function constants and relation constants must refer to
entities in the universe of discourse; and, yes, this departs from the
traditional semantics of first-order predicate calculus.)

$$i:{\cal O}\cup{\cal F}\cup{\cal R}\longrightarrow O$$

Second, the function must map object constants into objects, function constants
into functions, and relation constants into relations.  Notice that we allow for
functions and relations of arbitrary arity.  

\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^*$.
\medskip

Third, on all basic constants, $i$ must agree with the pairings described in
this document.  Note that, even with this restrictions, KIF is only a
``partially interpreted'' language -- the interpretations of some atoms (the
basic constants) are fixed in the definition of the language but the meanings of
other atoms (the non-basic constants) are left open (i.e. left to the
imaginations of the language users).

\subsect{Variable Assignment}

A {\it variable assignment} is a function that (1) maps individual variables
${\cal V}$ into elements of a universe of discourse $O$ and (2) maps sequence
variables ${\cal W}$ into sequences of elements.

$$v:{\cal V}\longrightarrow O$$

$$v:{\cal W}\longrightarrow O^*$$

The notion of a variable assignment is important in defining the meaning of
quantified terms and sentences and is discussed further in the section on
quantified expressions.

\subsect{Semantic Value}

Given an interpretation and a variable assignment, we can assign a {\it
semantic value} to every term in the language.  We formalize this as a
function $s_{iv}$ from the set ${\cal T}$ of terms into the set ${\cal O}$
of objects in the universe of discourse.

$$s_{iv}:{\cal T}\longrightarrow{\cal O}$$

\begconcept\defconcept{$\nu$}{individual variable}
If an expression is an individual variable $\nu$, the semantic value is the
element assigned to that variable by the given variable assignment.

$$s_{iv}(\nu)=v(\nu)$$
\endconcept

\begconcept\defconcept{$\sigma$}{object constant}
The semantic value of an object constant $\sigma$ is the object assigned to
that constant by the given interpretation.

$$s_{iv}(\sigma)=i(\sigma)$$
\endconcept

The semantic value of a non-atomic term depends on the structure of the term.  The
details are given in the following sections.

\subsect{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 into truth
values.

$$t_{iv}:{\cal S}\longrightarrow\{true,false\}$$

\begconcept\defconcept{$\lambda$}{logical constant}
The truth value of a logical constant is the truth value assigned by the
corresponding interpretation.

$$t_{iv}(\lambda)=i(\lambda)$$
\endconcept

The truth value of a non-atomic sentence depends on the structure of the
sentence.  The details are given in the following sections.

\subsect{Satisfaction}

The definition of truth value relies on both an interpretation for the constants
of KIF as well as 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 databases (i.e. sets of sentences), we say that an interpretation is a
model of a database if and only if it is a model of every sentence in the
database. 

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 a sentence
for one variable assignment, it satisfies it for every variable assignment.

The occurrence of a free variable in a sentence means that the sentence is true
for all assignments of the variable.  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 bound.  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)))}.

\subsect{Logical Entailment}

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 database, 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.

Given a database $\Delta$, we say that a database $\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.

\subsect{Epistemic Entailment}

We say that a database $\Delta$ {\it epistemically entails} a sentence $\phi$ if
and only if every model of $\Delta$ that maps the constant {\tt database} into
$\Delta$ is also a model of $\phi$.

{\it An indexical like this is important in our treatment of nonmonotonic
knowledge and also for problem solving control.  The question is whether we
should expand our indexicality.  Both Genesereth and Guha would like to see a
general indexical like {\tt now} that refers o the current situation.  With
this indexical, it would be possible to define {\tt database} as a function on
this situation, e.g. {\tt (database now)}.  It would also be possible to
condition the database on features other than its own contents.  There is
essentially no down side to this, given that we need some sort of indexicality
anyway.}

\vfill\eject

\sect{Functional Terms and Relational Sentences}

Functional terms and relational sentences are the simplest non-atomic expressions
in KIF.  We treat them together here because of the similarity between the
definition of semantic value for functional terms and the definition of truth
value for relational sentences.

\subsect{Functional Terms}

Recall that a functional term is an expression of the form shown below.  The atom
$\pi$ here is a function constant; $\tau_1,\ldots,\tau_k$ are terms; and
$\omega$ is an optional sequence variable.

\medskip
\centerline{\tt ($\pi$ $\tau_1$ ... $\tau_k$ $[\omega]$)}
\medskip

For example, assuming that {\tt salary}, {\tt +}, and {\tt *} are function
constants, the following expressions are all legal terms in KIF.

\medskip
\beginverbatim
(salary joe)

(+ 1 2 3)

(* $x $y $z)

(+ $x 2 3 $y @l)
\endverbatim
\medskip

Simple functional terms can be composed to form more complex functional terms, as
in the following examples.

\medskip
\beginverbatim
(* (salary joe) 2)

(+ (* a b) a)

(+ (* $x b @l) (salary joe) @m)
\endverbatim
\medskip

\begconcept

\defconcept{($\pi$ $\tau_1$ ... $\tau_k$)}{term}
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)]$$

\endconcept

As an example, let us consider the semantic value of the term {\tt (+ (* a b) a)},
given an interpretation $i$ that maps {\tt a} to the integer $2$, {\tt b} to $3$,
{\tt +} to the addition function on integers, and {\tt *} to the multiplication
function on integers.  With this interpretation, the semantic value of {\tt (* a
b)} is the product of $2$ and $3$, i.e. $6$.  The semantic value of {\tt (+ (* a b)
a)} is then just the sum of $6$ and $2$, i.e. $8$.

\begconcept

\defconcept{($\pi$ $\tau_1$ ... $\tau_k$ $[\omega]$)}{term}
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.

$$s_{iv}(\hbox{\tt ($\pi$ $\tau_1$...$\tau_n$ $\omega$)})=
i(\pi)[s_{iv}(\tau_1),...,s_{iv}(\tau_n)|s_{iv}(\omega)]$$

\endconcept

For example, if $i$ is an interpretation that maps {\tt a} to the integer $1$ and
{\tt @l} to the sequence of integers $\langle 2,3,4\rangle$, then the semantic
value of the term {\tt (+ a @l)} is the sum of $1$, $2$, $3$, and $4$, i.e. $10$.

\begconcept

\defconcept{(value $\tau$ $\tau_1$ ... $\tau_k$)}{term}

\defconcept{(value $\tau$ $\tau_1$ ... $\tau_k$ $\omega$)}{term}

\endconcept

\subsect{Relational Sentences}

The definition of truth value for relational sentences is analagous to the
definition of semantic value of functional terms.  Recall that a relational
sentence is an expression of the form shown below.  The atom $\rho$ here is a
relation constant; $\tau_1,\ldots,\tau_k$ are terms; and $\omega$ is an optional
sequence variable.

\medskip
\centerline{\tt ($\rho$ $\tau_1$ ... $\tau_k$ $[\omega]$)}
\medskip

\begconcept

\defconcept{($\rho$ $\tau_1$ ... $\tau_k$)}{sentence}
The truth value of a 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}$$

\midconcept

\defconcept{($\rho$ $\tau_1$ ... $\tau_k$ $[\omega]$)}{sentence}

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.

$$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}$$

\endconcept

\begconcept

\defconcept{(holds $\tau$ $\tau_1$ ... $\tau_k$)}{sentence}

\defconcept{(holds $\tau$ $\tau_1$ ... $\tau_k$ $\omega$)}{sentence}

\endconcept

\vfill\eject

\sect{Logical Terms and Sentences}

\subsect{Logical Terms}

\begconcept

\defconcept{(if $\phi$ $\tau_1$ $\tau_2$)}{term}

The semantic value of a simple conditional depends on the truth value of the
embedded sentence.  If the truth value of the 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.

$$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}$$

\endconcept

As an example, consider the term {\tt (if (> a 0) a (- a))}.  If the object
denoted by the constant {\tt a} and the object denoted by the constant {\tt 0}
satisfy the relation denoted by the relation constant {\tt >}, then the
semantic value of this term is the object denoted by {\tt a}; otherwise, it is
the semantic value of the term {\tt (- a)}.  Under the usual interpretation of
these symbols, the term denotes the absolute value of {\tt a}.

\begconcept

\defconcept{(cond $\phi_1$ $\tau_1$ ... $\phi_n$ $\tau_n$)}{term}

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 0.

$$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
0&otherwise\cr}$$

\endconcept

\subsect{Logical Sentences}

\begconcept

\defconcept{(not $\phi$)}{sentence}

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}$$

\midconcept

\defconcept{(and $\phi_1$ ... $\phi_n$)}{sentence}
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&$\forall j\;t_{iv}(\phi_j)=true$\cr
false&otherwise\cr}$$

\midconcept

\defconcept{(or $\phi_1$ ... $\phi_n$)}{sentence}

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&$\exists j\;t_{iv}(\phi_j)=true$\cr
false&otherwise\cr}$$

\midconcept

\defconcept{(=> $\phi_1$ ... $\phi_n$ $\phi$)}{sentence}

If the truth value of every antecedent in an implication is $true$, then the
the truth value of the implication as 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 $false$, regardless of the truth value of the
consequent.

$$t_{iv}(\hbox{\tt (=> $\phi_1$ ... $\phi_n$ $\phi$)})=\cases{
true&$\exists j\;t_{iv}(\phi_j)=false$ or $t_{iv}(\phi)=true$\cr
false&otherwise\cr}$$

\midconcept

\defconcept{(<= $\phi$ $\phi_1$ ... $\phi_n$)}{sentence}

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 $\exists j\;t_{iv}(\phi_j)=false$\cr
false&otherwise\cr}$$

\midconcept

\defconcept{(<=> $\phi_1$ $\phi_2$)}{sentence}

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}$$

\endconcept

\vfill\eject

\sect{Quantified Terms and Sentences}

The truth 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 versions of the
variable assignment.  We say that a variable assignment $v'$ is a {\it version}
of variable assignment $v$ with respect to $\tau$ if and only if $v'$ agrees
with $v$ on all variables except for the free variables in $\tau$.  The
assignments for the free variables in $\tau$ can be the same as those in $v$ or
can be completely different.

\subsect{Quantified Terms}

\begconcept

\defconcept{(lambda $\tau_1$ $\tau_2$)}{term}

\endconcept

\begconcept

\defconcept{(setof $\tau$ $\phi$)}{term}

\endconcept

\subsect{Quantified Sentences}

The truth 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.  We say that a variable assignment $v'$ is a {\it new
version} of variable assignment $v$ with respect to $\tau$ if and only if $v'$
agrees with $v$ on all variables except for the free variables in $\tau$.  The
assignments for the free variables in $\tau$ can be the same as those in $v$ or
can be completely different.

\begconcept

\defconcept{(exists $\tau$ $\phi$)}{sentence}
Given an interpretation $i$ and variable assignment $v$, the truth value of
an existentially quantified sentence 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 first argument.

$$t_{iv}(\hbox{\tt (exists $\tau$ $\phi$)})=\cases{
true&$\exists v'\;t_{iv'}(\phi)=true$\cr
false&otherwise\cr}$$

\midconcept

\defconcept{(forall $\tau$ $\phi$)}{sentence}
Given an interpretation $i$ and variable assignment $v$, the truth value of a
universally quantified sentence 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 the first argument.

$$t_{iv}(\hbox{\tt (forall $\tau$ $\phi$)})=\cases{
true&$\forall v'\;t_{iv'}(\phi)=true$\cr
false&otherwise\cr}$$

\endconcept

\vfill\eject

\sect{Knowledge about Knowledge}

\subsect{Metalinguistic Knowledge}

In formalizing knowledge about knowledge, we use a conceptualization in which
expressions are treated as objects in the universe of discourse and in which
there are functions and relations appropriate to these objects.  In our
conceptualization, we treat atoms as primitive objects (i.e. having no
subparts).  We conceptualize complex expressions (i.e. non-atoms) as lists of
subexpressions (either atoms or other complex expressions).  In particular, every
complex expression is viewed as a list of its immediate subexpressions.

For example, we conceptualize the sentence {\tt (not (p (+ a b c) d))} as a
list consisting of the operator {\tt not} and the sentence {\tt (p (+ a b c)
d)}.  This sentence is treated as a list consisting of the relation constant
{\tt p} and the terms {\tt (+ a b c)} and {\tt d}.  The first of these terms
is a list consisting of the function constant {\tt +} and the object constants
{\tt a}, {\tt b}, and {\tt c}.

For Lisp programmers, this conceptualization is relatively obvious, but it
departs from the usual conceptualization of formal languages taken in the
mathematical theory of logic.  It has the disadvantage that we cannot describe
certain details of syntax such as parenthesization and spacing (unless we
augment the conceptualization to include string representations of expressions
as well).  However, it is far more convenient for expressing properties of
knowledge and inference than string-based conceptualizations.

In order to assert properties of expressions in the language, we need a way of
referring to those expressions.  There are two ways of doing this in KIF.

One way is to use the {\tt quote} operator in front of an expression.  Formally, a
quotation denotes the expression embedded within the term.

\begconcept

\defconcept{(quote $\epsilon$)}{term}
$$s_{iv}(\hbox{\tt (quote $\epsilon$)})=\epsilon$$

\endconcept

Therefore, to refer to the symbol {\tt john}, we use the term {\tt 'john} or,
equivalently, {\tt (quote john)}.  To refer to the expression {\tt (p a b)}, we
use the term {\tt '(p a b)} or, equivalently, {\tt (quote (p a b))}.

With a way of referring to expressions, we can assert their properties.  For
example, the following sentence ascribes to the individual named {\tt john} the
belief that the moon is made of a particular kind of blue cheese.

\medskip
\beginverbatim
(bel john '(material moon stilton))
\endverbatim
\medskip

Note that, by nesting quotes within quotes, we can talk about quoted
expressions.  In fact, we can write towers of sentences of arbitrary heights, in
which the sentences at each level talk about the sentences at the lower levels.

Since expressions are first-order objects, we can quantify over them, thereby
asserting properties of whole classes of sentences.  For example, we could say
that Mary believes everything that John believes.  This fact together with the
preceding fact allows us to conclude that Mary also believes the moon to be made
of blue cheese.

\medskip
\beginverbatim
(=> (bel john $p) (bel mary $p))
\endverbatim
\medskip

The second way of referring to expressions is KIF is to use the {\tt list}
function.  

\begconcept

\defconcept{list}{relation constant}
A term that begins with {\it list} refers to the sequence of objects
denoted by the arguments in the term.

$$s_{iv}(\hbox{\tt (list $\tau_1$ ...$\tau_k$)})=\langle
s_{iv}(\tau_1),...,s_{iv}(\tau_k)\rangle$$

\endconcept

For example, we can denote a complex expression like {\tt (p a b)} by a term of
the form {\tt (list 'p 'a 'b)}, as well as {\tt '(p a b)}.

The advantage of the {\tt list} representation over the {\tt quote}
representation is that it allows us to quantify over parts of expressions.  For
example, let us say that Lisa is more skeptical than Mary.  She agrees with
John, but only on the composition of things.  The first sentence below asserts
this fact without specifically mentioning {\tt moon} or {\tt stilton}.  Thus, if
we were to later discover that John thought the sun to be made of chili peppers,
then Lisa would be constrained to believe this as well.

\medskip
\beginverbatim
(=>(bel john (list 'material $x $y))
   (bel lisa (list 'material $x $y)))
\endverbatim
\medskip

While the use of {\tt list} allows us to describe the structure of expressions
in arbitrary detail, it is somewhat awkward.  For example, the term {\tt (list
'material \$x \$y)} is somewhat awkward.  Fortunately, we can eliminate this
difficulty using backquote and comma.  Rather than using the {\tt list}
function constant as described above, we write the expression preceded by the
backquote character {\tt `} and add a comma character {\tt ,} in front of any
subexpression that is not to be taken literally.  For example, we would rewrite
the preceding sentence as follows.

\medskip
\beginverbatim
(=> (bel john `(material ,$x ,$y))
    (bel lisa `(material ,$x ,$y)))
\endverbatim
\medskip

This approach is particularly nice in that it parallels the treatment of quoting
and unquoting in Common Lisp.  However, a warning is in order.  All Common
Lisps translate quoted expressions into lists with {\tt quote} as the fist
element, e.g. {\tt '(f a)} translates into {\tt (quote (f a))}.  However, not all
Common Lisps are consistent in the handling of backquote.  Some Lisps translate
backquoted expressions into internal forms involving {\tt list}, e.g. {\tt `(f
,\$x)} translates into {\tt (list 'f \$x)}.  Some use {\tt cons}, e.g. {\tt (cons
'f (cons \$x nil))}.  Some use neither or a mixture.  This does not prohibit our
using the approach in KIF, but it means that we cannot rely on all Lisp readers to
produce the internal form we want.

In order to facilitate the encoding of knowledge about KIF, the language
includes the following type relations.

\begconcept

\defconcept{atom}{relation constant}
{The sentence {\tt (atom $\tau$)} means that the object denoted by $\tau$ is
an atom.}

\midconcept

\defconcept{indvarp}{relation constant}
{The sentence {\tt (indvarp $\tau$)} means that the object denoted by $\tau$
is an individual variable.}

\midconcept

\defconcept{listp}{relation constant}
{The sentence {\tt (listp $\tau$)} is true if $\tau$ is a list.}

\midconcept

\defconcept{(seqvarp $\tau$)}{relation constant}
{The sentence {\tt (seqvarp $\tau$)} means that the object denoted by $\tau$
is a sequence variable.}

\midconcept

\defconcept{(varp $\tau$)}{relation constant}
{The sentence {\tt (varp $\tau$)} means that the object denoted by $\tau$ is
a variable.}

\endconcept

\subsect{Changing Levels of Denotation}

The vocabulary introduced in the preceding subsection allows us to encode
properties of expressions in and of themselves.  In this section, we add some
vocabulary that allows us to change levels of denotation, i.e. to relate
expressions about expressions with the expressions they denote.

The first of these is the relation constant {\tt true}.  For example, we can say
that a sentence of the form {\tt (=> (p \$x) (q \$x))} is true by writing the
following metasentence.

\medskip
\beginverbatim
(true '(=> (p $x) (q $x)))
\endverbatim
\medskip

This may seem of limited utility, since we can just write the sentence denoted by
the argument as a sentence in its own right.  The advantage of the metanotation
becomes clear when we need to quantify over sentences, as in the encoding of axiom
schemas.  For example, we can say that every sentence of the form {\tt (=> $\phi$
$\phi$)} is true with the following metasentence.

\medskip
\beginverbatim
(=> (relconst $p) (true `(=> ,$p ,$p)))
\endverbatim
\medskip

Semantically, we would like to say that a sentence of the form {\tt (true '$\phi$)}
is true if and only if the sentence $\phi$ is true.  In other words, for any
interpretation and variable assignment, the truth value $t_{iv}(\hbox{\tt (true
'$\phi$)})$ is the same as the truth value $t_{iv}(\phi)$.  In other words, for
every truth function $t_{iv}$, {\tt true} is our language's name for $t_{iv}$.

Unfortunately, this causes serious problems.  Equating a truth function with
the meaning it ascribes to {\tt true} quickly leads to paradoxes.  Consider, for
example, the following sentence, which asserts that it itself is not true.  For
any truth function $t_{iv}$ that maps {\tt true} to itself, we get a
contradiction.  If $t_{iv}$ of the following sentence is $true$, then by the
rules for assignment of the logical operators contained in the sentence, we see
that $t_{iv}$ must make the sentence $false$.  If $t_{iv}$ assigns the value
$false$, then, again by the rules for assignment of the logical operators, we
see that it must assign it the value $true$.  In either case, we get a
contradication.

\medskip
\beginverbatim
This sentence is false.
\endverbatim
\medskip

Fortunately, we can circumvent such paradoxes by defining the meaning of {\tt
true} a little more narrowly.  Our definition is a little complicated, but it is
nice in that the intuitive interpretation of {\tt true} is almost always right,
yet paradoxes are completely avoided.

\begconcept

\defconcept{true}{relation constant}

We begin by considering a diminished language.  Let $\Sigma'$ be the set of
all constants in KIF except for {\tt true}, and let $i'$ be any
interpretation for the constants in $\Sigma'$.  We extend $i'$ to an
interpretation $i$ for all of the constants in KIF by assigning a meaning to
{\tt true} as well as the other constants in the language.

First, we define an infinite series of functions $i_n$; then we define
$i$ in terms of these functions.  All of the functions in the series agree with
$i'$ on the constants other than {\tt true}.

$$i_n(\sigma)=i'(\sigma)$$

Each $i_n$ maps {\tt true} into a partial function, i.e. it assigns truth
values to some sentences and not to others, and the function assigned to {\tt
true} by each succeeding $i_n$ agrees with the functions assigned by all
preceding $i_n$. Thus, the function assigned to {\tt true} by each $i_n$
is a refinement of the functions assigned by its predecessors.  We start off
this progression by having $i_0$ assign to {\tt true} a function that is
undefined on all sentences.

$$i_0(\hbox{\tt true})(\phi)=\bot$$

Next, we define the succeeding $i_n$ functions in terms of their
predecessors.

$$i_n(\hbox{\tt true})(\phi)=\cases{true&$\models_{i_{n-1}}\phi$\cr
false&$\models_{i_{n-1}}\hbox{\tt (not $\phi$)}$\cr
\bot&otherwise\cr}$$

Since $i_n(\hbox{\tt true})$ is a partial function, the ``interpretations''
are not really ``proper''; and, therefore, the notation
$\models_{i_{n-1}}\phi$ in this definition is inappropriate.  In using this
notation, we mean that interpretation $i_{n-1}$ satisfies $\phi$ if and only
if $\phi$ is satisfied by every proper interpretation (1) that is consistent
with $i_{n-1}$ and (2) that maps {\tt true} into a complete function.

Finally, we define an interpretation for the full KIF vocabulary in terms of our
$i_n$ functions.

$$i(\hbox{\tt true})(\phi)=\cases{true&$i_n(\hbox{\tt true})(\phi)=true$\cr
false&$i_n(\hbox{\tt true})(\phi)=false$\cr
anything&otherwise\cr}$$

\endconcept

Notice that this definition does not prescribe a truth value for
self-referential sentences.  In paradoxical cases (like the one cited
earlier), it is in fact necessary for an interpretation to assign a different
truth value to such sentences than the one assigned by the function it assigns
to {\tt true}.

%%% Do we want closure here too??

In order to change levels of denotation at the term level, KIF provides the
function constant {\tt denotation} (which gives the denotation of the expression
supplied as its argument) and {\tt name} (which gives the standard name of the
expression supplied as its argument).

\begconcept

\defconcept{(denotation $\tau$)}{function constant}
{The term {\tt (denotation $\tau$)} denotes the object denoted by the object
denoted by $\tau$.  A quotation denotes the quoted expression; a number,
character, or string denotes itself; the denotation of any other object is
$0$.}

\midconcept

\defconcept{(name $\tau$)}{function constant}
{The term {\tt (name $\tau$)} denotes the standard name for the object denoted
by the term $\tau$.  The standard name for a number, character, or string is
itself; the standard name for any other expression $\tau$ is {\tt (quote $\tau$)};
the standard name for any non-expression is at the discretion of the user. 
(Note that there are only a countable number of terms in KIF, but there can be
models with uncountable cardinality; consequently, it is not always possible
for every object in the universe of discourse to have a unique name.) }

\endconcept

{\it Discussion here of well-foundedness of these functions, to avoid
term-based paradoxes.}

\vfill\eject

\sect{Nonmonotonicity}

Many knowlege representation and reasoning systems are capable of drawing
conclusions based on the absence of knowedge from a database.  This is
nonmonotonic reasoning.  The addition of new sentences to the database
may be cause for the system to retract earlier conclusions.

In some systems, the exact policy for deriving nonmonotonic conclusions is
built into the system.  In other systems, the policy can be modified
by its user, though rarely within the system's knowledge representation
language (e.g. by selecting which predicates to circumscribe).  Since KIF
is a knowledge representation language and not a system, it is necessary
to provide means for its user to express his nomonotonic reasoning policy
within the language itself.

To this end, we define a new type of legal list expressions---{\it default
rules}. The syntax of defaults rules is described by the following modified
BNF:

\medskip
\beginverbatim
<defrule> ::= <sentence> | (<<= <sentence> <premise>*)

<premise> ::= <sentence> | (consis <sentence>)
\endverbatim
\medskip

The sentence that follows {\tt <<=} is the {\it consequent} of the rule;
the premises that are sentences are its {\sl prerequisites}, and the
premises that have the form {\tt (consis $\phi$)} are its {\it justifications}.
Notice that every sentence $\phi$ is also a default rule. The consequent
of this default is $\phi$ itself.

For instance, the default rule 

\medskip
\beginverbatim
(<<= (flies $x) (bird $x) (consis (flies $x)))
\endverbatim
\medskip

\noindent
expresses that an object can be assumed to fly if this object is known to be
a bird and it is consistent to assume that it flies.

A {\it nonmonotonic database} is a set of default rules. Since every
sentence is a default rule, every database (i.e. set of sentences) is a
nonmonotonic database. The semantics of default rules described at the end
of this section extends the notion of a model to nonmonotonic databases. We
say that a nonmonotonic database $\Delta$ {\it (nonmonotonically) entails}
a sentence $\phi$ if every model of $\Delta$ is also a model of $\phi$.
We will see that the definition of a model for nonmonotonic databases is
``nonlocal'': One cannot check whether an interpretation $i$ is a model by
looking at each default rule in isolation. This feature of the definition is
responsible for the nonmonotonic character of the new notion of entailment.

The use of {\tt consis} is the only source of nonmonotonicity in KIF.
Accordingly, a rule without justifications will be called
{\it monotonic}. This particularly simple case will be discussed first.

\subsect{Monotonic Rules}

It is clear that a monotonic rule is either a sentence or an expression of
the form
$$(\hbox{\tt <<= $\phi$ $\phi_1$ $\dots$ $\phi_n$}),$$
where $\phi$, $\phi_1,\dots,\phi_n$ are sentences. Such an expression should
be distinguished from the implication
$$(\hbox{\tt <= $\phi$ $\phi_1$ $\dots$ $\phi_n$}).$$
Monotonic rules are not sentences; they are similar to {\it inference rules},
familiar from elementary
logic. If, for instance, $\Delta$ consists of some sentences
$\Delta_0$ and one rule ({\tt <<=} $\psi$ $\phi$),
where $\phi$ and $\psi$ are sentences without free variables, then the set
of sentences entailed by  $\Delta$ is the smallest set of
sentences which (i) contains $\Delta_0$, (ii) is closed
under logical entailment, and (iii) contains $\psi$ provided that it
contains $\phi$.
It is not generally true that this set contains the implication
({\tt <=} $\psi$ $\phi$).

The rationale for using monotonic rules in knowledge representation,
instead of implications, is twofold. On the one hand, the ``directed''
character of rules can simplify the task of developing efficient inference
procedures. On the other hand, in some cases, replacing {\tt <==} by
{\tt <=} would be semantically unacceptable. For instance, the rules

\medskip
\beginverbatim
(<<= (status-known $x) (citizen $x))

(<<= (status-known $x) (not (citizen $x)))
\endverbatim
\medskip

\noindent
allow us to infer {\tt (status-known Joe)} only if one of the sentences

\medskip
\beginverbatim
(citizen Joe),  (not (citizen Joe))
\endverbatim
\medskip

\noindent
can be inferred.
Replacing the rules by implications would make {\tt (citizen \$x)}
identically true.

\subsect{Logic Programs}

A pure Prolog rule
$$\phi\hbox{\tt :-}\phi_1,\dots,\phi_n$$
where $\phi,\phi_1,\dots,\phi_n$ are atoms,
can be viewed as a syntactic variant of the monotonic rule
$$(\hbox{\tt <<= $\phi$ $\phi_1$ $\dots$ $\phi_n$})$$
except for two important details. First, the declarative semantics of
Prolog applies the {\it unique names assumption} to its ground
terms. If, for example, the program contains no function constants, then this
assumption can be expressed by the sentences
$$(\hbox{\tt not ($=$ $\sigma_1$ $\sigma_2$))}$$
for all distinct object constants $\sigma_1$, $\sigma_2$ in the language
of the program. Second, this semantics
applies the {\it closed world assumption} to each relation. For
a relation constant $\sigma$, this assumption can be expressed by the rule
$$(\hbox{\tt <<= (not ($\sigma$ $\nu$)) (consis (not ($\sigma$ $\nu$)))}),$$
where $\nu$ is a sequence variable. A pure Prolog program can be translated
into KIF by appending to it (i) the sentences expressing the unique names
assumption, and (ii) the default rules expressing the closed world assumption.

This method can be easily extended to programs with negation as failure.
A negative subgoal {\tt not}$\,\phi$ is represented in KIF by the premise
{\tt (consis (not $\phi$))}. (Adding {\tt consis} is necessary because,
in KIF, {\tt not} represents classical negation, rather than negation as
failure.)

\subsect{Circumscribing Abnormality}

Extending a set of sentences by the closed world assumption for some relation
constant $\sigma$, expressed by a default rule as shown above,
has the same effect as circumscribing $\sigma$ (with all object, function
and relation constants varied).  In particular, circumscribing
abnormality can be expressed by the default rule

$$\hbox{\tt (<<= (not (ab }\nu\hbox{\tt )) (consis (not (ab }\nu\hbox{))))}.$$

Consider, for instance, the nonmonotonic database that contains, in addition
to this standard default, two facts: {\tt (bird tweety)} and

\medskip
\beginverbatim
(<= (flies $x) (bird $x) (not (ab aspect1 $x)))
\endverbatim
\medskip

\noindent
(birds fly unless they are abnormal in {\tt aspect1}).
This database nonmonotonically entails the conclusion
that everything is {\it not} abnormal, including {\tt tweety}:

\medskip
\beginverbatim
(not (ab $x))
\endverbatim
\medskip

>From this, we can conclude that {\tt tweety} flies.

Suppose, on the other hand, that our database includes also the fact
that {\tt tweety} is abnormal in {\tt aspect1}:

\medskip
\beginverbatim
(ab aspect1 Tweety)
\endverbatim
\medskip

In this case, we can no longer infer that {\tt tweety} is not abnormal, and,
therefore, we cannot conclude that {\tt tweety} is a flier.  Note, however,
that we have {\it not} asserted that {\tt tweety} cannot fly; we have only
prevented the default rule from taking effect in this case.

\subsect{Semantics of Default Rules}

Recall that the truth value of a sentence is defined relative to an
interpretation $i$ and a variable assignment $v$. To define the truth
value of a premise in a default rule, we need to
select, instead of a single interpretation $i$, a {\it set} of
interpretations---the interpretations that are considered ``possible.''
In the following definition, $I$ is a set of interpretations which all have
the same universe of discourse $O$, and $v$ is a variable assignment with
this universe. We consider prerequisites and justifications separately.

\begconcept

\defconcept{\tt $\phi$}{premise}

The truth value of a prerequisite is {\it true}
if and only if it is true for at every ``possible'' intepretation.
$$t_{Iv}(\phi)=\cases{
true&$\forall i\in I\;t_{iv}(\phi)=true$\cr false&otherwise\cr}$$

\midconcept

\defconcept{\tt (consis $\phi$)}{premise}

The truth value of a justification is {\it true}
if and only if its second term is true for at least one ``possible''
intepretation.
$$t_{Iv}(\hbox{\tt (consis $\phi_i$)})=\cases{
true&$\exists i\in I\;t_{iv}(\phi)=true$\cr false&otherwise\cr}$$

\endconcept

Let $\Delta$  be a nonmonotonic database. We define when a set $I$ of
interpretations is ``a set of possible worlds'' for $\Delta$, by means
of the following fixpont construction. Consider a universe of discourse $O$;
by a {\it world} we understand an interpretation with the universe $O$.
Let $I$ be a set of worlds. Consider the largest set $I'$ of worlds such
that, for each default $\delta\in\Delta$ and each variable assignment $v$ with
the universe $O$, the following condition holds:
If the truth value of every prerequisite of $\delta$ for $I'$ and $v$ is
$true$, and the truth value of every justification of $\delta$ for $I$ and
$v$ is true, then the truth value of the consequent of $\delta$ for
$I'$ and $v$ is $true$. (This $I'$ always exists.) If $I'=I$, then we say
that $I$ is {\it a set of possible worlds} for $\Delta$. Typically, a
nonmonotonic database has many sets of possible worlds; it is clear, for
instance, that any two interpretations with different universes cannot
belong to the same set of possible worlds.

An interpretation $i$ is a {\it model} of $\Delta$ if it belongs to some set of
possible worlds for $\Delta$.

\vfill\eject

\sect{Modal Knowledge}

Epistemic modals are represented by metalevel terms, and we invent appropriate
relations on these sentences.

For example, we would write the fact that {\tt 2} is necessarily equal to {\tt
1+1} using the relation {\tt necessary}, as in the following sentence.

\medskip
\beginverbatim
(necessary '(= 2 (+ 1 1)))
\endverbatim
\medskip

We can represent possibility and other modalities in similar fashion.

\medskip

{\it On the assumption that epistemic modals are to be handled in this
manner, we need a proposal for a vocabulary and a semantics for that vocabulary.}

\vfill\eject

\sect{Terminological Knowledge}

KIF provides a set of definition operators for expressing "analytic
truths" (e.g., triangles have 3 sides).  Such "analytic definitions" are
in contrast to metalinguistic "substitutional definitions" that define
new object level syntax in a macro-like fashion.

{\it A proposal for substitional definitions is being prepared.  The
specifications for analytic definitions described in this section are
subject to further review and refinement.}


An analytic definition in KIF is a sentence that provides a category
declaration and definition for a non-basic constant.  Associated with
each analytic definition is a sentence called its {\it domain
assertion}.  The meaning of a definition is that its domain assertion is
true and that its domain assertion is an analytic truth.  Intuitively,
analytic truths are true by definition or by logical entailment from
other definitions.  For example, term subsumption in the KL-ONE family
of representation languages is analytic in that it is determined solely
on the basis of term definitions.  This notion of analytical truth is
expressed in KIF with the relation {\tt analytic-truth} as follows.

\begconcept

%\defconcept{(domain-assertion $\phi$)}{function constant}
%
%The term {\tt (domain-assertion $\phi$)} denotes the sentence that is
%the domain assertion of definition $\phi$.  The sentence denoted by {\tt
%domain-assertion} for each form of KIF definition is specified in the
%description of the definition forms.
%
%\midconcept
%
\defconcept{(analytic-truth $\phi$)}{relation constant}

Given a database $\delta$, the sentence {\tt (analytic-truth $\phi$)}
means that the sentence $\phi$ is logically entailed by the domain
assertions of the definitions that are logically entailed by database
$\delta$.

\endconcept

The definition forming operators available in KIF are as follows.

\begconcept

\defconcept{(defobject $\sigma$ $\phi_1$ ... $\phi_n$)}{definition}

New objects are defined using {\tt defobject}.  The first argument is the
name of the object being defined, and the remaining arguments are the sentences
constituting the object's definition.  The domain assertion of an object
definition is the conjunction of the sentences defining the object;
i.e.,

\medskip
\centerline{\tt (and~$\phi_1$~...~$\phi_n$)}
\medskip

\endconcept

For example, the following sentence defines the constant {\tt id} to be a left
and right identity for the binary function named {\tt f}.

\medskip
\beginverbatim
(defobject id
  (= (f $x id) $x)
  (= $x (f $x id)))
\endverbatim
\medskip

The domain assertion for that definition is:

\medskip
\beginverbatim
(and (= (f $x id) $x) (= $x (f $x id))
\endverbatim
\medskip

\begconcept

\defconcept{(defunction $\pi$ ($\nu_1$ ... $\nu_k$) $\tau$)}{definition}

New functions are defined using {\tt defunction}.  The first argument is the
name of the function being defined.  The second argument is a list of variables
corresponding to the arguments of the function.  The third argument is the term
defining the function.  The domain assertion of a function definition is
an equality those arguments are the second and third arguments of the
definition; i.e.,

\medskip
\centerline{\tt (=~($\pi$~$\nu_1$~...~$\nu_k$)~$\tau$)}
\medskip

\endconcept

For example, the following sentence defines the function {\tt
paternal-grand-father} in terms of the {\tt father} function.

\medskip
\beginverbatim
(defunction paternal-grand-father ($x) (father (father $x)))
\endverbatim
\medskip

The domain assertion for that definition is:

\medskip
\beginverbatim
(= (paternal-grand-father $x) (father (father $x)))
\endverbatim
\medskip

\begconcept

\defconcept{(defrelation $\rho$ ($\nu_1$ ... $\nu_k$) $\phi_1$ ... $\phi_n$)}{definition}

New relations can be defined using {\tt defrelation}.  The first
argument is the name of the relation.  The second argument of a list of
variables corresponding to the arguments of the relation.  The remaining
arguments are the sentences defining the relation.  The domain assertion
of a relation definition is a biconditional involving the relation being
defined and the sentences defining the relation as follows:

\medskip
\centerline{\tt (<=>~($\rho$~$\nu_1$~...~$\nu_k$)~(and~$\phi_1$~...~$\phi_n$))}
\medskip

\endconcept

For example, the following sentence defines a bachelor to be an
unmarried male.

\medskip 
\beginverbatim
(defrelation bachelor ($x) (male $x) (not (married $x)))
\endverbatim
\medskip

The domain assertion for that definition is:

\medskip
\beginverbatim 
(<=> (bachelor $x) (and (male $x) (not (married $x))))
\endverbatim
\medskip

A {\it primitive relation} is one for which we do not have an {\it if and only
if} definition.

\begconcept

\defconcept{(defprimrelation $\rho$ ($\nu_1$ ... $\nu_k$) $\phi_1$ ...
$\phi_n$)}{definition}

New primitive relations are defined using {\tt defprimrelation}.  The
first argument is the name of the relation.  The second argument of a
list of variables corresponding to the arguments of the relation.  The
remaining arguments are the sentences defining the relation.  The domain
assertion of a relation definition is a conditional involving the
relation being defined and the sentences defining the relation as
follows:

\medskip
\centerline{\tt (=>~($\rho$~$\nu_1$~...~$\nu_k$)~(and~$\phi_1$~...~$\phi_n$))}
\medskip

\endconcept

For example, the following sentence defines a {\tt person} to be a
mammal, but does not include any other information about persons.

\medskip
\beginverbatim
(defprimrelation person ($x) (mammal $x))
\endverbatim
\medskip

The difference between the definition of a primitive relation and a
non-primitive relation is that, in the former case, the implication
defining the relation is unidirectional, whereas, in the latter case, it
is bidirectional.  Thus, the domain assertion for the above definition
of {\tt person} is:

\medskip
\beginverbatim
(=> (person $x) (mammal $x))
\endverbatim
\medskip

\vfill\eject

\sect{Certainty Factors}

KIF is a two-valued logic.  Given an interpretation and a variable assignment,
every sentence must be either $true$ or $false$.  The problem is that, in many
applications, it is useful to work with a larger set of truth values. 
Fortuately, we can accommodate such extended truth value sets without changing
the logic, by encoding truth values at the metalevel.  In the following
paragraphs, we illustrate this approach for the case of Bayesian probabilities.

We express the probability of a sentence by writing an equation involving the
function constant {\tt probability}.

\begconcept

\defconcept{probability}{function constant}

The term {\tt (probability $\tau$ $\tau_1$ ... $\tau_n$)} denotes the
probability of the sentence denoted by $\tau$ {\it given that} the sentences
denoted by $\tau_1$, ..., $\tau_n$ are all true.  If $n=0$, then the term
denotes the prior probability of the sentence denoted by $\tau$.

\endconcept

For example, the following sentence states that the prior
probability of {\tt bird-23} being black is 0.2.

\medskip
\beginverbatim
(= (probability '(black bird-23)) 0.2)
\endverbatim
\medskip

We express probability intervals by asserting inequalities involving the {\tt
probability} function.

\medskip
\beginverbatim
(>= (probability '(black bird-23)) 0.1)

(=< (probability '(black bird-23)) 0.9)
\endverbatim
\medskip

Conditional probabilities are represented using a multi-argument version of
{\tt probability}.  The following sentence states that the conditional
probability of {\tt bird-23} being black, {\it given that} it is a raven, is
0.9.

\medskip
\beginverbatim
(= (probability '(black bird-23) '(raven bird-23)) 0.9)
\endverbatim
\medskip

The semantics of probabilities can be captured by writing appropriate metalevel
axioms.

For example, we can mix logical conclusions with probabilities by writing
sentences like the ones shown below.  The first sentence asserts that the
probability of any tautology is 1.0.  The second sentence asserts that the
negation of a tautology has probability 0.0.  The third sentence asserts the
equiprobability of logically equivalent sentences.

\medskip
\beginverbatim
(=> (tautology $p) (= (probability $p) 1.0))

(=> (tautology $p) (= (probability `(not ,$p)) 0.0))

(=> (tautology `(<=> ,$p ,$q)) (= (probability $p) (probability $q)))
\endverbatim
\medskip

Similarly, we can encode standard properties of probabilities, such as Bayes's
Rule.

\medskip
\beginverbatim
(= (probability $q $p)
   (/ (* (probability $p $q) (probability $q)) (probability $p)))
\endverbatim
\medskip

Other approaches to the representation of uncertainty can be handled in similar
fashion.  The important thing  here is that KIF allows for the definition of
different schemes for encoding uncertainty.

\medskip

{\it On the assumption that numerical uncertainties are to be handled in this
manner, we need a proposal for a vocabulary and a semantics for that vocabulary.}

\vfill\eject

\sect{Numbers}

{\it KIF includes the following standard vocabulary for describing
properties of numbers.  As a start, we include all of the side-effect-free
functions and relations defined in Common Lisp.  At the moment, this
section is simply a list of vocabulary items.  Ultimately, it should
contain a more structured summary, like that in the Common Lisp manual.}

\begconcept

\defconcept{*}{function constant}
The term {\tt (* $\tau_1 \ldots \tau_n$)} denotes the product of the
objects denoted by $\tau_1$ through $\tau_n$.

\midconcept

\defconcept{+}{function constant}
{The term {\tt (+ $\tau_1 ... \tau_n$)} denotes the sum of the objects denoted by $\tau_1$
through $\tau_n$.}

\midconcept

\defconcept{-}{function constant}
{The term {\tt (- $\tau_1 ... \tau_n$)} denotes the difference between the object denoted
by $\tau_1$ and the objects denoted by $\tau_2$ through $\tau_n$.  An exception
occurs when $n=1$, in which case the term denotes the negation of $\tau_1$.}

\midconcept

\defconcept{/}{function constant}
{The term {\tt (/ $\tau_1 \ldots \tau_n$)} denotes the result of dividing the object denoted
by $\tau_1$ by the remaining objects denoted by $\tau_2$ through $\tau_n$.}

\midconcept

\defconcept{1+}{function constant}
{The term {\tt (1+ $\tau$)} denotes the object denoted by $\tau$ plus one.}

\midconcept

\defconcept{1-}{function constant}
{The term {\tt (1- $\tau$)} denotes the object denoted by $\tau$ minus one.}

\midconcept

\defconcept{abs}{function constant}
{The term {\tt (abs $\tau$)} denotes the absolute value of the object denoted by $\tau$.}

\midconcept

\defconcept{acos}{function constant}
{The term {\tt (acos $\tau$)} denotes the arc cosine of the object denoted by $\tau$
(in radians).} 

\midconcept

\defconcept{acosh}{function constant}
{The term {\tt (acosh $\tau$)} denotes the arc cosine of the object denoted by $\tau$
(in radians).}

\midconcept

\defconcept{ash}{function constant}
{The term {\tt (ash $\tau_1$ $\tau_2$)} denotes the result of arithmetically shifting
the object denoted by $\tau_1$ by the number of bits denoted by $\tau_2$ (left
or right shifting depending on the sign of $\tau_2$).}

\midconcept

\defconcept{asin}{function constant}
{The term {\tt (asin $\tau$)} denotes the arc sine of the object denoted by $\tau$ (in
radians).}
\midconcept

\defconcept{asinh}{function constant}
{The term {\tt (asinh $\tau$)} denotes the hyperbolic arc sine of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{atan}{function constant}
{The term {\tt (atan $\tau$)} denotes the arc tangent of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{atanh}{function constant}
{The term {\tt (atanh $\tau$)} denotes the hyperbolic arc tangent of the object denoted by
$\tau$ (in radians).}

\midconcept

\defconcept{boole}{function constant}
{The term {\tt (boole $\tau$ $\tau_1$ $\tau_2$)} denotes the result of applying
the operation denoted by $\tau$ to the objects denoted by $tau_1$ and
$-\tau_2$.} 

\midconcept

\defconcept{ceiling}{function constant}
{The term {\tt (ceiling $\tau$)} denotes the smallest integer greater than the object denoted by $\tau$.}

\midconcept

\defconcept{cis}{function constant}
{The term {\tt (cis $\tau$)} denotes the complex number denoted by $cos(\tau) + i
sin(\tau)$. The argument is any non-complex number of radians.}

\midconcept

\defconcept{complex}{function constant}
{The term {\tt (complex <realpart> <imagpart>)} denotes the complex number with the real and imaginary
parts denoted by {\tt realpart} and {\tt imagpart}.}

\midconcept

\defconcept{conjugate}{function constant}
{The term {\tt (conjugate $\tau$)} denotes the complex conjugate of the number denoted by $\tau$.}

\midconcept

\defconcept{cos}{function constant}
{The term {\tt (cos $\tau$)} denotes the cosine of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{cosh}{function constant}
{The term {\tt (cosh $\tau$)} denotes the hyperbolic cosine of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{decode-float}{function constant}
{The term {\tt (decode-float $\tau$)} denotes the mantissa of the object denoted by $\tau$.}

\midconcept

\defconcept{denominator}{function constant}
{The term {\tt (denominator $\tau$)} denotes the denominator of the canonical reduced form of
the object denoted by $\tau$.}

\midconcept

\defconcept{exp}{function constant}
{The term {\tt (exp $\tau$)} denotes $e$ raised to the power the object denoted by $\tau$.}

\midconcept

\defconcept{expt}{function constant}
{The term {\tt (expt <base> <power>)} denotes the object denoted by {\tt <base>} raised to the
power the object denoted by {\tt <power>}.}

\midconcept

\defconcept{fceiling}{function constant}
{The term {\tt (fceiling $\tau$)} denotes the smallest integer (as a floating point number) greater than
the object denoted by $\tau$.}

\midconcept

\defconcept{ffloor}{function constant}
{The term {\tt (ffloor $\tau$)} denotes the largest integer (as a floating point number) less than
the object denoted by $\tau$.}

\midconcept

\defconcept{float}{function constant}
{The term {\tt (float $\tau$)} denotes the floating point number equal to the object denoted by
$\tau$.}

\midconcept

\defconcept{float-digits}{function constant}
{The term {\tt (float-digits $\tau$)} denotes the number of digits used in the representation
of a floating point number denoted by $\tau$.}

\midconcept

\defconcept{float-precision}{function constant}
{The term {\tt (float-precision $\tau$)} denotes the number of significant digits
in the floating point number denoted by $\tau$.}

\midconcept

\defconcept{float-radix}{function constant}
{The term {\tt (float-radix $\tau$)} denotes the radix of the 
floating point number denoted by $\tau$. The most common values are 2 and 16.}

\midconcept

\defconcept{float-sign}{function constant}
{The term {\tt (float-sign <float1> <float2>)} denotes a floating-point number with the
same sign as the object denoted by {\tt <float1>} and the same absolute value as
the object denoted by {\tt <float2>}.}

\midconcept

\defconcept{floor}{function constant}
{The term {\tt (floor $\tau$)} denotes the largest integer less than the object denoted by
$\tau$.}

\midconcept

\defconcept{fround}{function constant}
{The term {\tt (fround $\tau$)} is equivalent to {\tt (ffloor (+ 0.5 $\tau$))}.}

\midconcept

\defconcept{ftruncate}{function constant}
{The term {\tt (ftruncate $\tau$)} denotes the largest integer (as a floating point number)
less than the object denoted by $\tau$.}

\midconcept

\defconcept{gcd}{function constant}
{The term {\tt (gcd $\tau_1 \ldots \tau_n$)} denotes the greatest common divisor of the
objects denoted by $\tau_1$ through $\tau_n$.}

\midconcept

\defconcept{imagpart}{function constant}
{The term {\tt (imagpart $\tau$)} denotes the imaginary part of the object denoted by $\tau$.}

\midconcept

\defconcept{integer-decode-float}{function constant}
{The term {\tt (integer-decode-float $\tau$)} denotes the significand of the object denoted by $\tau$.}

\midconcept

\defconcept{integer-length}{function constant}
{The term {\tt (integer-length $\tau$)} denotes the number of bits required to store the
absolute magnitude of the object denoted by $\tau$.}

\midconcept

\defconcept{isqrt}{function constant}
{The term {\tt (isqrt $\tau$)} denotes the integer square root of the object denoted by $\tau$.}

\midconcept

\defconcept{lcm}{function constant}
{The term {\tt (lcm $\tau_1 \ldots \tau_n$)} denotes the least common multiple of the
objects denoted by $\tau_1,\ldots,\tau_n$.}

\midconcept

\defconcept{log}{function constant}
{The term {\tt (log <number> <base>)} denotes the logarithm of the object denoted by {\tt <number>} in the
base denoted by {\tt base}.}

\midconcept

\defconcept{logand}{function constant}
{The term {\tt (logand $\tau_1 \ldots \tau_n$)} denotes the bit-wise logical and of the objects denoted
by $\tau_1$ through $\tau_n$.}

\midconcept

\defconcept{logandc1}{function constant}
{The term {\tt (logandc1 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logand (lognot
$\tau_1$ $\tau_2$)}.}

\midconcept

\defconcept{logandc2}{function constant}
{The term {\tt (logandc2 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logand $\tau_1$ $\tau_2$))}.}

\midconcept

\defconcept{logcount}{function constant}
{The term {\tt (logcount $\tau$)} denotes the number of {\it on} bits in the object denoted
by $\tau$. If the denotation of $\tau$ is positive, then the one bits are counted;
otherwise, the zero bits in the twos-complement representation are counted.}

\midconcept

\defconcept{logeqv}{function constant}
{The term {\tt (logeqv $\tau_1 \ldots \tau_n$)} denotes the logical-exclusive-or of the
objects denoted by $\tau_1,\ldots,\tau_n$.}

\midconcept

\defconcept{logior}{function constant}
{The term {\tt (logior $\tau_1 \ldots \tau_n$)} denotes the bit-wise logical inclusive or of the
objects denoted by $\tau_1$ through $\tau_n$. It denotes 0 if there are no arguments.}

\midconcept

\defconcept{lognand}{function constant}
{The term {\tt (lognand $\tau_1$ $\tau_2$)} is equivalent to {\tt (lognot
(logand $\tau_1$ $\tau_2$))}.}

\midconcept

\defconcept{lognor}{function constant}
{The term {\tt (lognor $\tau_1$ $\tau_2$)} is equivalent to {\tt (not (logior $\tau_1$
$\tau_2$))}.}
\midconcept

\defconcept{lognot}{function constant}
{The term {\tt (lognot $\tau$)} denotes the bit-wise logical not of the object denoted by $\tau$.}

\midconcept

\defconcept{logorc1}{function constant}
{The term {\tt (logorc1 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logior (lognot
$\tau_1$) $\tau_2$)}.}

\midconcept

\defconcept{logorc2}{function constant}
{The term {\tt (logorc2 $\tau_1$ $\tau_2$)} is equivalent to {\tt (logior
$\tau_1$ (lognot $\tau_2$))}.}

\midconcept

\defconcept{logxor}{function constant}
{The term {\tt (logxor $\tau_1 \ldots \tau_n$)} denotes the bit-wise logical exclusive or of
the objects denoted by $\tau_1$ through $\tau_n$. It denotes 0 if there are no arguments.}

\midconcept

\defconcept{max}{function constant}
{The term {\tt (max $\tau_1 \ldots \tau_n$)} denotes the largest object denoted by $\tau_1$ through
$\tau_n$.}

\midconcept

\defconcept{min}{function constant}
{The term {\tt (min $\tau_1 \ldots \tau_n$)} denotes the smallest object denoted by $\tau_1$ through
$\tau_n$.}

\midconcept

\defconcept{mod}{function constant}
{The term {\tt (mod <number> <divisor>)} denotes the root of the object denoted by {\tt <number>}
modulo the object denoted by {\tt <divisor>}. The result will have the same sign as
the object denoted by {\tt <number>}.}

\midconcept

\defconcept{numerator}{function constant}
{The term {\tt (numerator $\tau$)} denotes the numerator of the canonical reduced form of
the object denoted by $\tau$.}

\midconcept

\defconcept{phase}{function constant}
{The term {\tt (phase $\tau$)} denotes the angle part of the polar representation of 
the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{rational}{function constant}
{The term {\tt (rational $\tau$)} denotes the standard rational representation of the object
denoted by $\tau$ (any non-complex number).}

\midconcept

\defconcept{rationalize}{function constant}
{The term {\tt (rationalize $\tau$)} denotes the rational representation of the object
denoted by $\tau$.}

\midconcept

\defconcept{realpart}{function constant}
{The term {\tt (realpart $\tau$)} denotes the real part of the object denoted by $\tau$.}

\midconcept

\defconcept{rem}{function constant}
{The term {\tt (rem <number> <divisor>)} denotes the remainder of the object denoted by
{\tt <number>} divided by the object denoted by {\tt <divisor>}. The result has
the same sign as the object denoted by {\tt <divisor>}.}

\midconcept

\defconcept{round}{function constant}
{The term {\tt (round $\tau$)} denotes the integer nearest to the object denoted by $\tau$.
If the object denoted by $\tau$ is halfway between two integers (for example 3.5),
it denotes the nearest integer divisible by 2.}

\midconcept

\defconcept{scale-float}{function constant}
{The term {\tt (scale-float <float> <power>)} denotes a floating-point number that is the
representational radix of the object denoted by {\tt <float>} raised to the integer 
denoted by {\tt <power>}.}

\midconcept

\defconcept{signum}{function constant}
{The term {\tt (signum $\tau$)} denotes the sign of the object denoted by $\tau$. This is one of -1,
1, or 0 for rational numbers, and one of -1.0, 1.0, or 0.0 for floating point numbers.}

\midconcept

\defconcept{sin}{function constant}
{The term {\tt (sin $\tau$)} denotes the sine of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{sinh}{function constant}
{The term {\tt (sinh $\tau$)} denotes the hyperbolic sine of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{sqrt}{function constant}
{The term {\tt (sqrt $\tau$)} denotes the principal square root of the object denoted by $\tau$.}

\midconcept

\defconcept{tan}{function constant}
{The term {\tt (tan $\tau$)} denotes the tangent of the object denoted by $\tau$ (in radians).}

\midconcept

\defconcept{tanh}{function constant}
{The term {\tt (tanh $\tau$)} denotes the hyperbolic tangent of the object denoted by
$\tau$ (in radians).}

\midconcept

\defconcept{truncate}{function constant}
{The term {\tt (truncate $\tau$)} denotes the largest integer less than the object denoted
by $\tau$.}

\endconcept

Relations on numbers.

\begconcept

\defconcept{complexp}{relation constant}
{The sentence {\tt (complexp $\tau$)} means that the object denoted by $\tau$ is
a complex number.}

\midconcept

\defconcept{evenp}{relation constant}
{The sentence {\tt (evenp $\tau$)} means that the object denoted by $\tau$ is an even integer.}

\midconcept

\defconcept{floatp}{relation constant}
{The sentence {\tt (floatp $\tau$)} means that the object denoted by $\tau$ is a floating point
number.}

\midconcept

\defconcept{integerp}{relation constant}
{The sentence {\tt (integerp $\tau$)} means that the object denoted by $\tau$ is an integer.}

\midconcept

\defconcept{logbitp}{relation constant}
{The sentence {\tt (logbitp <index> <n>)} is true if bit {\tt <n>} of {\tt <index>} is 1.}

\midconcept

\defconcept{logtest}{relation constant}
{The sentence {\tt (logtest <n1> <n2>)} is true if the logical {\it and} of the two's-complement
representation of the integers {\tt <n1>} and {\tt <n2>} is not zero.}

\midconcept

\defconcept{minusp}{relation constant}
{The sentence {\tt (minusp $\tau$)} means that the object denoted by $\tau$ is a negative number.}

\midconcept

\defconcept{numberp}{relation constant}
{The sentence {\tt (numberp $\tau$)} means that the object denoted by $\tau$ is a number.}

\midconcept

\defconcept{oddp}{relation constant}
{The sentence {\tt (oddp $\tau$)} means that the object denoted by $\tau$ is an odd integer.}

\midconcept

\defconcept{plusp}{relation constant}
{The sentence {\tt (plusp $\tau$)} means that the object denoted by $\tau$ is a positive
number.}

\midconcept

\defconcept{rationalp}{relation constant}
{The sentence {\tt (rationalp $\tau$)} means that the object denoted by $\tau$ is a rational
number.}

\midconcept

\defconcept{zerop}{relation constant}
{The sentence {\tt (zerop $\tau$)} means that the term $\tau$ denotes 0.}

\midconcept

\defconcept{<}{relation constant}
{The sentence {\tt (< $\tau_1$ $\tau_2$)} is true if and only if the number denoted by
$\tau_1$ is less than the number denoted by $\tau_2$.}

\midconcept

\defconcept{=}{relation constant}
{The sentence {\tt (= $\tau_1$ $\tau_2$)} is true if and only if the terms $\tau_1$ and
$\tau_2$ refer to the same object.}

\midconcept

\defconcept{/=}{relation constant}
{The sentence {\tt (/= $\tau_1$ $\tau_2$)} is true if and only if the terms $\tau_1$ and
$\tau_2$ refer to different objects.}

\midconcept

\defconcept{=<}{relation constant}
{The sentence {\tt (=< $\tau_1$ $\tau_2$)} is true if and only if the number denoted by
$\tau_1$ is equal to or less than the number denoted by $\tau_2$.}

\midconcept

\defconcept{>}{relation constant}
{The sentence {\tt (> $\tau_1$ $\tau_2$)} is true if and only if the number denoted by
$\tau_1$ is greater than the number denoted by $\tau_2$.}

\midconcept

\defconcept{>=}{relation constant}
{The sentence {\tt (>= $\tau_1$ $\tau_2$)} is true if and only if the number denoted by
$\tau_1$ is greater than or equal to the number denoted by $\tau_2$.}

\endconcept

\vfill\eject

\sect{Lists}

{\it Ditto for lists.  The following are the side-effect-free subroutines in
Common Lisp appropriate to lists and sequences.}

\begconcept
\difconcept{adjoin}{function constant}
\difconcept{append}{function constant}
\difconcept{butlast}{function constant}
\difconcept{caaaar}{function constant}
\difconcept{caaadr}{function constant}
\difconcept{caaar}{function constant}
\difconcept{caadar}{function constant}
\difconcept{caaddr}{function constant}
\difconcept{caadr}{function constant}
\difconcept{caar}{function constant}
\difconcept{cadaar}{function constant}
\difconcept{cadadr}{function constant}
\difconcept{cadar}{function constant}
\difconcept{caddar}{function constant}
\difconcept{cadddr}{function constant}
\difconcept{caddr}{function constant}
\difconcept{cadr}{function constant}
\difconcept{car}{function constant}
\difconcept{cdaaar}{function constant}
\difconcept{cdaadr}{function constant}
\difconcept{cdaar}{function constant}
\difconcept{cdadar}{function constant}
\difconcept{cdaddr}{function constant}
\difconcept{cdadr}{function constant}
\difconcept{cdar}{function constant}
\difconcept{cddaar}{function constant}
\difconcept{cddadr}{function constant}
\difconcept{cddar}{function constant}
\difconcept{cdddar}{function constant}
\difconcept{cddddr}{function constant}
\difconcept{cdddr}{function constant}
\difconcept{cddr}{function constant}
\difconcept{cdr}{function constant}
\difconcept{cons}{function constant}
\difconcept{eighth}{function constant}
\difconcept{endp}{function constant}
\difconcept{eq}{function constant}
\difconcept{eql}{function constant}
\difconcept{equal}{function constant}
\difconcept{equalp}{function constant}
\difconcept{fifth}{function constant}
\difconcept{first}{function constant}
\difconcept{fourth}{function constant}
\difconcept{intersection}{function constant}
\difconcept{last}{function constant}
\difconcept{list}{function constant}
\difconcept{list*}{function constant}
\difconcept{list-length}{function constant}
\difconcept{make-list}{function constant}
\difconcept{ninth}{function constant}
\difconcept{nth}{function constant}
\difconcept{nthcdr}{function constant}
\difconcept{rest}{function constant}
\difconcept{revappend}{function constant}
\difconcept{second}{function constant}
\difconcept{set-difference}{function constant}
\difconcept{set-exclusive-or}{function constant}
\difconcept{seventh}{function constant}
\difconcept{sixth}{function constant}
\difconcept{subst}{function constant}
\difconcept{tenth}{function constant}
\difconcept{third}{function constant}
\difconcept{union}{function constant}
\difconcept{concatenate}{function constant}
\difconcept{count}{function constant}
\difconcept{count-if}{function constant}
\difconcept{count-if-not}{function constant}
\difconcept{elt}{function constant}
\difconcept{find}{function constant}
\difconcept{find-if}{function constant}
\difconcept{find-if-not}{function constant}
\difconcept{length}{function constant}
\difconcept{map}{function constant}
\difconcept{mapc}{function constant}
\difconcept{mapcan}{function constant}
\difconcept{mapcar}{function constant}
\difconcept{mapcon}{function constant}
\difconcept{mapl}{function constant}
\difconcept{maplist}{function constant}
\difconcept{merge}{function constant}
\difconcept{position}{function constant}
\difconcept{position-if}{function constant}
\difconcept{position-if-not}{function constant}
\difconcept{reduce}{function constant}
\difconcept{remove}{function constant}
\difconcept{remove-duplicates}{function constant}
\difconcept{remove-if}{function constant}
\difconcept{remove-if-not}{function constant}
\difconcept{reverse}{function constant}
\difconcept{search}{function constant}
\difconcept{sort}{function constant}
\difconcept{stable-sort}{function constant}
\difconcept{subseq}{function constant}
\difconcept{substitute}{function constant}
\difconcept{substitute-if}{function constant}
\difconcept{substitute-if-not}{function constant}
\difconcept{member}{relation constant}
\difconcept{null}{function constant}
\difconcept{subsetp}{relation constant}
\difconcept{every}{relation constant}
\difconcept{notany}{relation constant}
\difconcept{notevery}{relation constant}
\difconcept{some}{relation constant}
\endconcept

\vfill\eject

\sect{Knowledge About Procedures}

\subsect{Partial Programs}

One of the primary uses of declarative databases is the control of agents,
i.e. entities that can observe and act as well as reason.  Robots are 
good examples of agents.  They observe their environments via touch sensors,
video cameras, infrared detectors, etc.; and they act on their environments by
moving their arms, their grippers, their wheels, etc.  Expert consultation
systems can also be viewed as agents.  They print out questions and
results, and they read the answers entered by the user.  Even individual Lisp
programs can profitably be thought of as agents.  They sense their environments
(e.g. by accessing global variables), and they are capable of having side effects
on those environments (e.g. by setting the values of global variables).

An agent's observation of its environment at each point in time is one of a 
fixed (but possibly very large) set of {\it percepts} (determined by its sensory
hardware).  Its effect on the environment at each point in time is one of a
predetermined set of {\it actions} (determined by its effectory hardware).  In
the context of Lisp, actions are individual Lisp subroutine calls, and percepts
are the results of executing those subroutines.  For example, the act of applying
Lisp's {\it read} subroutine is an action, and the resulting value is the
subsequent percept.

For a machine with a set $A$ of actions, we define a procedure to be a function
from the natural numbers into $A$, which maps each time step into the action to
be performed on that step.  A {\it generalized procedure} is a function that 
maps each time step into an action {\it or} another procedure (which is run to
completion before considering the next step of the outer procedure).

A {\it KIF program} is a description of a generalized procedure in KIF.  In
writing a KIF program, we select a term (usually a constant) to denote the
procedure being defined.  We then write axioms characterizing the function
constituting the procedure.

\begconcept

\defconcept{action}{function constant}
The term {\tt (action $\tau_1$ $\tau_2$)} denotes the action prescribed by
the procedure named $\tau_1$ on the step of operation denoted by $\tau_2$.

\midconcept

\defconcept{percept}{function constant}
The term {\tt (percept $\tau_1$ $\tau_2$)} denotes the percept observed
during the execution of the procedure named $\tau_1$ on the step of operation
denoted by $\tau_2$.

\midconcept

\defconcept{call}{function constant}
The term {\tt (call $\tau$ $\tau_1$ ... $\tau_n$)} denotes the action of
applying the subroutine named $\tau$ to the arguments denoted by $\tau_1$,
..., $\tau_n$.

\endconcept

As an illustration of our formalization of programs, consider a procedure for
controlling the pressure in a reservoir.  Let us assume that the reservoir has an
inlet that adds material (and thereby tends to drive the pressure up), a drain
that removes material (and thereby tends to drive the pressure down), and a
customer that also removes material (and thereby tends to drive the pressure
down).  In order to control the pressure, we have a number of actions at our
disposal.  We can temporarily close the inlet; we can temporarily open the drain;
or we can do nothing.  The percept on each step is the current pressure in the
reservoir as value.

We start off by writing a sentence to interpret our machine's percepts.  If the
value on a step exceeds 100 psi, then we know that a high pressure
situation exists.  

\medskip
\beginverbatim
(<= (high-pressure $n)
    (= (percept $n) $z)
    (> $z 100))
\endverbatim
\medskip

In order to characterize our program {\tt program-1}, we write a single general
axiom.  The action on the $n$-th step of operation is any action that is {\tt
doable} and cannot be shown to be {\tt bad}.  The concepts {\tt doable} and {\tt
bad} are axiomatized below.   (The interpreter knows nothing about these concepts
except for the axioms provided by the KIF programmer.)

\medskip
\beginverbatim
(<- (action program-1 $n)
    (oneof $a (and (doable $a $n)
                   (not (provable (bad $a $n)))))
\endverbatim
\medskip

As mentioned in the problem description, there are three possible actions.  By
asserting the following sentences, we are stating that these actions are
doable on every step of operation.

\medskip
\beginverbatim
(doable (call 'noop) $n)

(doable (call 'shut-inlet) $n)

(doable (call 'open-drain) $n)
\endverbatim
\medskip

In some reasoning systems, the mention of an action automatically leads
to the execution of that action, whenever that occurrence is processed by the
reasoning system.  That is not the case with KIF.  The term {\tt (call
'shut-inlet)} simply {\it refers} to the action of shutting the inlet.

Although all three of our actions are doable, some are better than others in
certain situations.  For example, it is a bad idea to do nothing if the reservoir
exhibits high pressure.  

\medskip
\beginverbatim
(<= (bad (call 'noop) $n)
    (high-pressure $n))
\endverbatim
\medskip

Another way for an action to be bad is if there is a doable action that is
preferred.  Closing the inlet is better than opening the drain, because it
does not waste material.

\medskip
\beginverbatim
(<= (bad $b $n)
    (doable $a $n)
    (better $a $b))

(better (call 'shut-inlet) (call 'open-drain))
\endverbatim
\medskip

It is a simple matter to build an interpreter for KIF programs.  Consider one such
interpreter, called {\tt interpret}.  It takes a term and a theory as arguments and
executes the procedure denoted by the specified term and described in the specified
theory.   The operation of the interpreter is a simple ``observe-think-act''
loop.  On each cycle of operation, it observes the environment to get a percept
$x$ and draws conclusions by forward chaining from a sentence of the form {\tt (=
(percept $n$) $x$)}, where $n$ is the number of the cycle.  It then computes an
action to be executed by backward chaining to find a value for a term of the form
{\tt (action $p$ $n$)}, where $p$ is the name of the procedure.  If the action is a
{\tt return} action, the interpreter halts and returns the argument of the {\tt
return} action.  If no action is found, the interpreter halts unsuccessfully. 
Otherwise, the action is executed, and the cycle repeats.

Now, we can run our program.  Since we do not have a real reservoir at our
disposal, we can simulate one by defining our actions so that their sole effects
are to make adjustments on a fictional pressure variable.  In this case, we use
the atom {\tt *pressure*} and initialize the pressure to be 95 pounds per square
inch.  By executing the {\tt noop} action, {\it we} are not changing the state of
affairs in the reservoir.  However, the pressure still rises due to the open
inlet.  By executing the {\tt shut-inlet} action, we stop the pressure rise, and
the customer's demand on the reservoir causes the pressure to fall 30 pounds per
square inch.  Similarly, by executing the {\tt open-drain} action, we stop the
pressure rise, and the customer's demand causes the pressure to fall 30 pounds per
square inch.

\medskip
\beginverbatim
User: (defvar *pressure* 95)
Lisp: *PRESSURE*

User: (defun noop () (setq *pressure* (+ *pressure* 10)))
Lisp: NOOP

User: (defun shut-inlet () (setq *pressure* (- *pressure* 30)))
Lisp: SHUT-INLET

User: (defun open-drain () (setq *pressure* (- *pressure* 30)))
Lisp: OPEN-DRAIN
\endverbatim
\medskip

Now, we call {\tt interpret} on our program and watch the results.  The
initial percept is 0.  (Remember that a percept in Lisp is the value
returned by the preceding action.  Since there is no preceding action on the
first step, this percept is simply a default value.)  The first action in this
case is {\tt noop}.  This results in a pressure rise to 105 psi, the percept
for the second step.  In this case, {\tt noop} is a bad action, due to the
high pressure; and, following its program, the system decides to temporarily
close the inlet.  This results in a pressure drop on the third step, leading
to a sequence of {\tt noop} actions.  And so forth.

\medskip
\beginverbatim
User: (interpret 'program-1)

Percept: 0
Action:  (CALL 'NOOP)

Percept: 105
Action:  (CALL 'SHUT-INLET)

Percept: 75
Action:  (CALL 'NOOP)

Percept: 85
Action:  (CALL 'NOOP)

Percept: 95
Action:  (CALL 'NOOP)

Percept: 105
Action:  (CALL 'SHUT-INLET)

*** Computation aborted ***
\endverbatim
\medskip

If the system does not behave as desired, it is possible to tune its behavior
by adding additional facts to the theory describing our procedure.  For
example, we may get information about additional actions that are doable; we
may get more information about which actions are bad in and of themselves; and we
may get more information about which actions are better than others.

While this example is very simple, partial programming methodology can be used
in extremely complicated applications as well.  It allows the smooth blending of
seemingly disparate programming techniques -- such as Lisp programming,
object-oriented programming, and production systems.  The next section
illustrates the use of partial programming on a more complicated example.

{\it On the assumption that partial programs can be handled in this
manner, we need a proposal for a vocabulary and a semantics for that vocabulary.}

\subsect{Production Systems}

{\it It is a relatively easy matter to define condition action rules along
the lines decsribed in the preceding section.  For example, the following.

\medskip
\beginverbatim
(-=> (high-pressure) (call 'open-drain))
\endverbatim
\medskip

Conflict resolution can also be handled in terms of {\tt good} and {\tt bad}
actions.  And so forth.

On the assumption that production systems can be handled in this manner, we
need a proposal for a vocabulary and a semantics for that vocabulary.}

\subsect{Problem Solving Control}

An important use of the metalevel capabilities of KIF is in the formalization of
rules of inference.  For example, the following sentence formalizes the ordered
resolution rule of inference for ground clauses.  If the first literals in two
clauses are complementary, then it is legal to conclude the clause consisting of
the remaining literals of each clause.  (Adding unification to this formalization
to handle non-ground clauses presents no serious problems.)

\medskip
\beginverbatim
(<= (resolution (list 'or $p @l)
                (list 'or (list 'not $p) @m)
                (list 'or @n))
    (= (append (list @l) (list @m)) (list @n)))
\endverbatim
\medskip

With this information, it is possible for the system to answer metalevel
questions about resolution, like the one shown below.

\medskip
\beginverbatim
(resolution '(or p q) '(or (not p) (not r)) '(or q (not r)))
\endverbatim
\medskip

Starting with rules of inference formalized in this way, we can build up to
entire inference procedures.  One application of this ability is to characterize
the beliefs of resource-limited agents.  It also gives us a flexible way of
specifying inference procedures.  

As an example of this latter capability, consider the problem of writing a simple
resolution theorem-proving system.  The system should be capable of finding the
contradiction in databases of ground clauses, such as the following.

\medskip
\beginverbatim
(or p q)

(or (not p) (not r))

(or (not p))

(or (not q))
\endverbatim
\medskip

Our approach is to write the system as a KIF program, in a manner similar to
that described in the preceding section.  The difference is that the objects
being manipulated are databases, and the actions are database additions and
deletions.  In this case, we will use the single action {\tt save}.

Our first axiom, as before, defines the action of our program on the $n$-th step
to be any action that is doable and not provably bad.  The database on the
$n$-th step is found by applying the {\tt contents} function to the target
theory.

\medskip
\beginverbatim
(<- (action program-2 $n)
    (oneof $a (and (doable $a $n)
                   (not (provable (bad $a $n))))))

(<- (database $n) (eval '(contents 'database)))
\endverbatim
\medskip

There are two types of doable actions.  Our agent can return {\tt true} if the
database contains an empty disjunction (equivalent to a contradiction).  It can
also add a sentence to the theory, provided that the sentence is a
conclusion of two sentences already in the theory.

\medskip
\beginverbatim
(<= (doable (return true) $n)
    (member '(or) (database $n))))

(<= (doable (call 'save $r 'database) $n)
    (member $p (database $n))
    (member $q (database $n))
    (resolution $p $q $r))
\endverbatim
\medskip

Not all doable actions are equally good.  We do not want to waste time adding a
sentence to the database if it is already there.  We also do not want to do an
action if there is a better action to do.  It is better to return
successfully, if that action is doable, then to go on drawing conclusions.

\medskip
\beginverbatim
(<= (bad (call 'save $r 'database) $n)
    (member $r (database $n)))

(<= (bad $b $n)
    (doable $a $n)
    (better $a $b))

(better (return $x) (call 'save $p 'database))
\endverbatim
\medskip

We now have enough information to try out our agent.  We call {\tt interpret} on
the name of our program.  The database does not contain an empty disjunction; and
so it cannot return just yet.  By examining the sentences in the database and
using the definition of {\tt resolution} given earlier, it finds several possible
deductions.  It takes the first of these (involving the first two clauses in the
{\tt database} theory) and adds the consequence to the database.  On the second
step, this deduction is still valid but the conclusion is not added to the
database again because it is already contained therein and, therefore, that action
is bad.  The next possible conclusion is, therefore, considered.  The interpreter
then finds and adds a third conclusion, viz. {\tt (list 'or)}.  On the fourth
step, a {\tt return} action becomes doable (due to the manifest contradiction),
and the process halts.

\medskip
\beginverbatim
User: (interpret 'program-2)
Action: (CALL 'SAVE (LIST 'OR 'Q '(NOT R)) 'DATABASE)
Action: (CALL 'SAVE (LIST 'OR 'Q) 'DATABASE)
Action: (CALL 'SAVE (LIST 'OR) 'DATABASE)
Action: (RETURN TRUE)
Lisp: TRUE
\endverbatim
\medskip

Looking at the performance of our program, we may find that we really want
something different.  Let us say, for example, that we preferred to have
the agent draw short conclusions before long ones (in the hope that a
contradiction will be found faster that way).  We can easily modify our program
to do this by simply adding an additional axiom.  The following sentence asserts
that one conclusion is better than another if it is shorter.

\medskip
\beginverbatim
(<= (better (call 'save (list 'or @l) 'database)
            (call 'save (list 'or @m) 'database))
    (< (length (list @l)) (length (list @m))))
\endverbatim
\medskip

Having added this sentence, we can rerun our example.  This time the first
conclusion is bypassed in favor of the second conclusion, since the second
conclusion is shorter.

\medskip
\beginverbatim
User: (interpret 'program-2)
Action: (CALL 'SAVE (LIST 'OR 'Q) 'DATABASE)
Action: (CALL 'SAVE (LIST 'OR) 'DATABASE)
Action: (RETURN TRUE)
Lisp: TRUE
\endverbatim
\medskip

In similar fashion, it is possible to augment our program to include additional
rules of inference (to implement nonmonotonic reasoning, for example).  We can
add additional constraints on conclusions (e.g. probabilities, branchiness,
etc.).  We can also make available additional actions (e.g. asking questions
of the user, as in consultation systems).

Of course, the version of resolution shown here is not a particularly efficient
implementation.  However, it is easy to tune it up.  For example, instead of
searching linearly through the facts in the {\tt database} theory, we could use
an associative indexing scheme.  We could cache possible conclusions, so they need
not be recomputed on every step.  And so forth.

\medskip

{\it On the assumption that problem solving control can be defined in this
manner, we need a proposal for a vocabulary and a semantics for that vocabulary.}

\subsect{Lisp Programs}

\begconcept

\defconcept{eval}{function constant}
{The term {\tt (eval $\tau$)} denotes the value of applying the Lisp evaluator
to the expression denoted by $\tau$.}

\midconcept

\defconcept{lisp}{function constant}
{The term {\tt (lisp $\tau$)} denotes the procedure that in Lisp is expressed
by the list structure denoted by $\tau$.}

\endconcept

\vfill\eject

\nosect{References}

\bibitem{fikes}{fikes}Fikes, R., MacGregor, R., Brachman, R.: ``Strawman
Proposal'', DARPA Knowledge Representation Standards Workshop, March 1990.

\bibitem{genesrereth}{genesereth}Genesereth, M. R., Gruber, T., Guha, R. V.,
Letsinger, R., Singh, N.: ``Knowledge Interchange Format'', Logic-89-13,
Stanford University Computer Science Department, October 1989.

\bibitem{macgregor}{macgregor}MacGregor, R., Bates, R.: ``The Loom Knowledge
Representation Language'', USC/ISI Reprint Series ISI/RS-87-188, 1987.

\vfill\eject

\nosect{A. Dictionary of Reserved Words}

This appendix contains descriptions for constants that are being considered for
inclusion in the standard.  Users of the standard are not required to
abide by the semantics described here.  However, insofar as the
words are likely to become part of the standard, it is best either to adhere to
the semantics or avoid using them altogether.

\nosect{A.1 Object Constants}

\nosect{A.2 Function Constants}

\nosect{A.3 Relation Constants}

\begconcept

\defconcept{alike}{relation constant}
{The sentence {\tt (alike $\tau_1$ $\tau_2$)} is true if and only if the terms $\tau_1$ and
$\tau_2$ refer to the same object.  We include {\tt alike} as a special constant
in KIF to allow the user to prescribe that, in trying to prove the equivalence of
$\tau_1$ and $\tau_2$, an inference procedure is expected to try unifying
$\tau_1$ and $\tau_2$.}

\midconcept

\defconcept{is}{relation constant}
{The sentence {\tt (is $\tau_1$ $\tau_2$)} is true if and only if the terms $\tau_1$ and
$\tau_2$ refer to the same object.  The basic semantics of {\tt is} is the
same as that for {\tt =}.  We include {\tt is} as a special constant
in KIF to allow the user to prescribe that, in trying to prove the equivalence of
$\tau_1$ and $\tau_2$, an inference procedure is expected to evaluate $\tau_1$
and $\tau_2$ and then try unifying the resulting expressions.}

\midconcept

\defconcept{<-}{relation constant}
{The sentence {\tt (<- $\tau_1$ $\tau_2$)} is true if and only if the terms $\tau_1$ and
$\tau_2$ refer to the same object.  The basic semantics of {\tt <-} is the
same as that for {\tt =}.  We include {\tt <-} as a special constant in KIF to
allow the user to prescribe that this equation is to be used in one direction
only.}

\midconcept

\defconcept{<--}{relation constant}
{The sentence {\tt (<-- $\tau_1$ $\tau_2$)} is true if and only if the terms $\tau_1$ and
$\tau_2$ refer to the same object.  The basic semantics of {\tt <--} is the
same as that for {\tt =}.   We include {\tt <--} as a special constant in KIF to
allow the user to prescribe that this equation is to be used in one direction
only.  It differs from {\tt <-} in that an inference procedure processing it is
expected to cache its result (as an equation using the {\tt =} constant).}

\endconcept

\nosect{A.4 Logical Constants}

\begconcept

\defconcept{cut}{relation constant}
{The sentence {\tt cut} denotes the positive truth value.  We include {\tt cut} as a special
constant in KIF to allow the user to prescribe that, in the course of trying to
prove a literal, an inference procedure is expected to cut off all other ways of
trying to prove that literal so that, if the current method fails, the procedure
ceases to work on that literal.}

\endconcept

\nosect{A.5 Term Operators}

\nosect{A.6 Sentence Operators}

\begconcept

\defconcept{<==}{operator}
{The sentence {\tt (<== $\phi$ $\phi_1$ ... $\phi_n$)} is true if and only if
the sentence  $\phi$ is implied by the sentences $\phi_1$ through $\phi_n$. 
The basic semantics of {\tt <==} is the same as that for {\tt <=}.  We include
{\tt <==} as an operator in KIF to allow the user to prescribe that $\phi$ is to
be cached if it is ever proven.}

\midconcept

\defconcept{==>}{operator}
{The sentence {\tt (==> $\phi_1$ ... $\phi_n$ $\phi$)} is true if and only if the sentences
$\phi_1$ through $\phi_n$ imply the sentence $\phi$.  The basic semantics of {\tt
==>} is the same as that for {\tt =>}.  We include {\tt ==>} as an operator in
KIF to allow the user to prescribe that the $\phi$ is to be cached if it is
proven.} 

\endconcept

\bye

\subsect{Knowledge of Agents}

We use the relation {\tt knows} to assert that an agent knows a fact.
For example, to say that John knows that Mary is poor, we would write the
following sentence.

\medskip
\beginverbatim
(knows john '(poor mary))
\endverbatim
\medskip

Of course, knowledge-asserting sentences can be nested in arbitrary ways.  We can 
say that Mary knows that John knows that she is poor as follows.

\medskip
\beginverbatim
(knows mary '(knows john '(poor mary)))
\endverbatim
\medskip

We can capture the meaning of knowledge by writing axioms about the {\tt knows}
relation.  In the next few paragraphs, we encode the 5 most common axioms, which
jointly constitute the logical system S5.

If an agent knows somethings, it ought to be able to derive conclusions from
that knowledge.  In particular, it should be able to use Modus Ponens.  The {\it
distribution axiom}, which asserts this property, can be formalized as shown
below.

\medskip
\beginverbatim
(=> (knows $a $p) (knows $a `(=> ,$p ,$q)) (knows $a $q))
\endverbatim
\medskip

The {\it knowledge axiom} asserts that any sentence an agent knows to be true
must, in fact, be true.

\medskip
\beginverbatim
(=> (knows $a $p) (true $p))
\endverbatim
\medskip

The {\it positive introspection axiom} asserts that, if an agent knows something,
then it knows that it knows it.

\medskip
\beginverbatim
(=> (knows $a $p) (knows $a `(knows ,(name $p))))
\endverbatim
\medskip

The {\it negative introspection axiom} asserts that, if an agent does not know
something, then it knows that it does not know it.

\medskip
\beginverbatim
(=> (not (knows $a $p)) (knows $a `(not (knows ,(name $p)))))
\endverbatim
\medskip

The {\it epistemic necessitation axiom} guarantees that an agent knows all
sentences that are logically necessary.

\medskip
\beginverbatim
(=> (tautology $p) (knows $a $p))
\endverbatim
\medskip

\medskip

{\it On the assumption that knowledge operators are to be handled in this
manner, we need a proposal for a vocabulary and a semantics for that vocabulary.}

\vfill\eject

%%%%%%%%%%%%%%%%

Not all knowledge encoding tasks require that we consider all conceivable objects
in the universe; in some cases, some objects are relevant and others are
irrelevant.  For example, number theorists are usually concerned with the
properties of numbers and are not concerned with physical objects such as
resistors and transistors.  Electrical engineers are concerned with resistors
and transistors and are usually not concerned with bridges and buildings.  The
set of objects about which knowledge is being expressed in a database is called
the {\it object basis set} (or, synonymously, the {\it universe of discourse}).

A function is one kind of interrelationship among objects in a universe of
discourse.  Although we can define many functions for a given set of objects,
in conceptualizing an application world we usually emphasize some functions and
ignore others.  The set of functions in a conceptualization is called the {\it
functional basis set}.  

A  relation is another kind of interrelationship among objects in a
universe of discourse.  As we do with functions, in conceptualizing an
application world, we emphasize some relations and ignore others.  The set of
relations in a conceptualization is called the {\it relational basis set}.

%%%%%%%%%%%%%%%%

\nosect{A. KIF Dictionary}

This appendix gives the semantics for the basic constants and operators of KIF.

\nosect{A.1 Object Constants}

All Lisp numbers, characters, and strings are basic object constants in KIF.

\nosect{A.2 Function Constants}

\nosect{A.3 Relation Constants}

\nosect{A.4 Logical Constants}

\begconcept

\defconcept{false}
{{\tt false} denotes the negative truth value.}

\medconcept

\defconcept{true}
{{\tt true} denotes the positive truth value.}

\endconcept

\nosect{A.5 Term Operators}

\begconcept

\defconcept{cond}
{{\tt (cond $\phi_1$ $\tau_1$ ... $\phi_n$ $\tau_n$)} denotes
the value of the first term $\tau_i$ for which the corresponding expression
$\phi_i$ is true.}

\defconcept{if}
{{\tt (if $\phi$ $\tau_1$ $\tau_2$)} denotes the value of the expression
$\tau_1$ if the expression $\phi$ is true; otherwise, it denotes the  value of
the expression $\tau_2$.}

\defconcept{quote}
{{\tt (quote $\tau$)} denotes the expression $\tau$ literally.  Remember that the
expression {\tt '$\tau$} is equivalent to {\tt (quote $\tau$)}.}

\egroup

\nosect{A.6 Sentence Operators}

\bgroup
\parskip=10pt
\hangindent=\parindent

\defconcept{and}
{{\tt (and $\phi_1$ ... $\phi_n$)} is true if and only if all of the
specified sentences are true.}

\defconcept{defunction}
{{\tt (defunction $\pi$ ($\nu_1$ ... $\nu_k$) $\tau$)} is true if and only if
the function $\pi$ applied to $\nu_1$ ... $\nu_k$ is equal to $\tau$
for all values of the variables $\nu_1$ ... $\nu_k$.}

\defconcept{defobject}
{{\tt (defobject $\sigma$ $\phi_1$ ... $\phi_n$)} is true if and only if the
sentences $\phi_1$ ... $\phi_n$ (which constrain the object constant $\sigma$) are
all true.}

\defconcept{defprimrelation}
{{\tt (defprimrelation $\rho$ ($\nu_1$ ... $\nu_k$) $\phi_1$ ... $\phi_n$)} is
true if and only if the relation $\rho$ applied to $\nu_1$ ... $\nu_k$
is true whenever the sentences $\phi_1$ ... $\phi_n$ are true.}

\defconcept{defrelation}
{{\tt (defrelation $\rho$ ($\nu_1$ ... $\nu_k$) $\phi_1$ ... $\phi_n$)} is
true if and only if the relation $\rho$ applied to $\nu_1$ ... $\nu_k$
implies that the sentences $\phi_1$ ... $\phi_n$ are all true.}

\defconcept{exists}
{{\tt (exists $\tau$ $\phi$)} is true if and only if there is an assignment for
the free variables in the expression $\tau$ that makes the expression $\phi$
true.}

\defconcept{forall}
{{\tt (forall $\tau$ $\phi$)} is true if and only if the expression $\phi$ is
true for every assignment of the free variables in the expression $\tau$.}

\defconcept{not}
{{\tt (not $\phi$)} is true if and only if the expression $\phi$ is not true.}

\defconcept{or}
{{\tt (or $\phi_1$ ... $\phi_n$)} is true if and only if at least one of the
specified expressions is true.}

\defconcept{<=}
{{\tt (<= $\phi$ $\phi_1$ ... $\phi_n$)} is true if and only if the sentence
$\phi$ is implied by the sentences $\phi_1$ through $\phi_n$, i.e.
it is true if and only if $\phi$ is true or at least one $\phi_i$ is false..}

\defconcept{<=>}
{{\tt (<=> $\phi_1$ $\phi_2$)} is true if and only if the sentences $\phi_1$
and $\phi_2$ are equivalent.}

\defconcept{=>}
{{\tt (=> $\phi_1$ ... $\phi_n$ $\phi$)} is true if and only if the sentences
$\phi_1$ through $\phi_n$ imply the sentence $\phi$, i.e. it is true if and
only if $\phi$ is true or at least one $\phi_i$ is false.} 

\egroup
\vfill\eject

Although it is possible to define definitional relations like these without
changing the logic of KIF, we include definitional operators in the basic syntax,
because of their exceptional usefulness.

$$T_n=closure\{\phi|\models_{i_{n-1}}\phi\}$$

$$F_n=closure\{\phi|\models_{i_{n-1}}\hbox{\tt (not $\phi$)}\}$$

{\it Vladimir Lifschitz} points out a drawback of this approach to encoding
global assumptions.  When a knowledge base builder makes an assumption of
this sort, he sometimes intends it relative to his own
database.  In the approach described here, the object constant {\tt database}
refers to the entire database, which could be much larger than the original if
the original database is combined with others.  A possible solution to this is
to allow the knowledge base writer or translator to encode 

