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 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 uparrow and comma. Rather than using the listof function constant as described above, we write the expression preceded by the uparrow 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)))
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 relation.
(indvar (quote v))For every sequence variable s, there is an axiom asserting that it is a sequence variable. Each such axiom is a defining axiom for the seqvar relation.
(indvar (quote s))For every word w, there is an axiom asserting that it is a word. Each such axiom is a defining axiom for the word relation.
(word (quote w))Using this basic vocabulary and our vocabulary for lists, it is possible to define type relations for all types of syntactic expressions in KIF.
(=> (and (r 0) (forall (?n) (=> (r ?n) (r (1+ ?n))))) (forall (?n) (r ?n)))This schema encodes infinitely many sentences, the principle of mathematical induction for named relations. The following sentences are instances.
(=> (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 describe sentences in a language, but they are not themselves sentences in the language. As a result, they cannot be manipulated by procedures designed to process the language (presentation, storage, communication, deduction, and so forth) but instead must be hard coded into those procedures.
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 (=> p p) is true with the following sentence. (The relation sentence can easily be defined in terms of quote, listof, indvar, seqvar, and word.
(=> (sentence ?p) (wtr ^(=> ,?p ,?p)))Semantically, we would like to say that a sentence of the form (wtr 'p) is true if and only if the sentence p is true. Unfortunately, this causes serious problems. Equating a truth function with the meaning it ascribes to wtr quickly leads to paradoxes. The English sentence ``This sentence is false.'' illustrates the paradox. We can write this sentence in KIF as shown below. The sentence, in effect, asserts its own negation.
(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 not contain any occurrences of wtr. For all p that do contain occurrences, wtr is false.
(<=> (wtr 'p) p)With this modified definition, the paradox described above disappears, yet we retain the ability to write virtually all useful axiom schemata as metalevel axioms.
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 t. A quotation denotes the quoted expression; the denotation of any other object is bottom. As with wtr, the dentotation of a quoted expression is the embedded expression, provided that the expression does not contain any occurrences of denotation. Otherwise, the value is undefined.
(= (denotation 't) t)The term (name t) denotes the standard name for the object denoted by the term t. The standard name for an expression t is (quote t); the standard name for a 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 worlds with uncountable cardinality; consequently, it is not always possible for every object to have a unique name.)