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

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

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

For every individual variable ` v`, there is an axiom asserting that
it is indeed an individual variable. Each such axiom is a defining axiom for the

(indvar (quoteFor every sequence variablev))

(indvar (quoteFor every words))

(word (quoteUsing this basic vocabulary and our vocabulary for lists, it is possible to define type relations for all types of syntactic expressions in KIF.w))

(=> (and (This schema encodes infinitely many sentences, the principle of mathematical induction for named relations. The following sentences are instances.r0) (forall (?n) (=> (r?n) (r(1+ ?n))))) (forall (?n) (r?n)))

(=> (and (p 0) (forall (?n) (=> (p ?n) (p (1+ ?n))))) (forall (?n) (p ?n))) (=> (and (q 0) (forall (?n) (=> (q ?n) (q (1+ ?n))))) (forall (?n) (q ?n)))Axiom schemata are differentiated from axioms due to the presence of metavariables or other metalinguistic notation (such as dots or star notation), together with conditions on the variables. They

As we have seen, it is possible in KIF to write expressions that describe KIF sentences. As it turns out, there is also a way to write sentences that assert the truth of the sentences so described. The effect of adding such metalevel sentences to a knowledge base is the same as directly including the (potentially infinite) set of described sentences in the knowledge base.

The use of such a language simplifies the construction of knowledge-based systems, since it obviates the need for building axiom schemata into deductive procedures. It also makes it possible for systems to exchange axiom schemata with each other and thereby promotes knowledge sharing.

The KIF truth predicate is called `wtr` (which stands for ``weakly
true''). For example, we can say that a sentence of the form `(=> (p ?x) (q
?x))` is true by writing the following sentence.

(wtr '(=> (p ?x) (q ?x)))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 schemata. For example, we can say that every sentence of the form

(=> (sentence ?p) (wtr ^(=> ,?p ,?p)))Semantically, we would like to say that a sentence of the form

(wtr (subst (name ^(subst (name x) ^x ^(truth ,x))) ^x ^(not (wtr (subst (name x) ^x ^(not (wtr ,x)))))))No matter how we interpret this sentence, we get a contradiction. If we assume the sentence is true, then we have a problem because the sentence asserts its own falsity. If we assume the sentence is false, we also have a problem because the sentence then is necessarily true.

Fortunately, we can circumvent such paradoxes by slightly modifying the proposed
definition of `wtr`. In particular, we have the following axiom schema
for all ` p` that do

(<=> (wtr 'With this modified definition, the paradox described above disappears, yet we retain the ability to write virtually all useful axiom schemata as metalevel axioms.p)p)

From the point of view of formalizing truth, `wtr` is a cheat, since it
fails to cover those interesting cases where sentences contain the truth
predicate. However, from the point of view of capturing axiom schemata
*not* involving the truth predicate, it works just fine. Furthermore,
unlike the solutions to the problem of formalizing truth, the framework
presented here is easy for users to understand, and it is easy to implement.

Two other constants round out KIF's level-crossing vocabulary.

The term `(denotation t)` denotes the object denoted by the object
denoted by

(= (denotation 'The termt)t)

Michael R. Genesereth , Stanford University, genesereth@cs.stanford.edu