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.