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 `(not (p (+ a b c) d))` as a
list consisting of the operator `not` and the sentence `(p (+ a b c)
d)`. This sentence is treated as a list consisting of the relation constant
`p` and the terms `(+ a b c)` and `d`. The first of these terms
is a list consisting of the function constant `+` and the object constants
`a`, `b`, and `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 `quote` operator in front of an expression. From the
section on semantics, we know that a quotation denotes the expression embedded
within the term. Therefore, to refer to the symbol `john`, we use the term
`'john` or, equivalently, `(quote john)`. To refer to the expression
`(p a b)`, we use the term `'(p a b)` or, equivalently, `(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 `john` the
belief that the moon is made of a particular kind of blue cheese.

(believes john '(material moon stilton))

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.

(=> (believes john ?p) (believes mary ?p))

The second way of referring to expressions is KIF is to use the `listof`
function. For example, we can denote a complex expression like `(p a b)` by
a term of the form `(listof 'p 'a 'b)`, as well as `'(p a b)`.

The advantage of the `listof` representation over the `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 `moon` or `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.

(=> (believes john (listof 'material ?x ?y)) (believes lisa (listof 'material ?x ?y)))

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

(=> (believes john `(material ,?x ,?y)) (believes lisa `(material ,?x ,?y)))

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 `quote` as the
first element, e.g. `'(f a)` translates into `(quote (f a))`.
However, not all Common Lisps are consistent in the handling of
backquote. Some Lisps translate backquoted expressions into internal
forms involving `listof`, e.g. ``(f ,?x)` translates into `(listof 'f ?x)`. Some use `cons`, e.g. `(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.

Wed Dec 7 13:23:42 PST 1994