The first method is use of <charref> syntax, i.e. the characters # and \, followed by the character to be represented.
While this method works for all 128 characters, it is less than ideal for documents like this one, because of the difficulty of writing out non-printing characters. Using this method, it is also difficult to assert properties of some classes of characters. For this reason, KIF supports an alternative method of specification, viz. the use of the 7 bit code corresponding to the character. The relationship between characters and their numerical codes is given via the functions char-code and code-char. The former maps the nth character cn into the corresponding 7-bit integer n, and the latter maps a 7-bit integer n into the corresponding character cn. The values of these functions on all other arguments are undefined.
(= (char-code #\cn) n)
(= (code-char n) #\cn)
The relation constant character is true of the characters of KIF
and no other objects.
One way of referring to strings is through the use of the <string> syntax described in chapter 2. In this method, we refer to the string abc by enclosing it in double quotes, i.e. "abc".
A second way is through the use of character blocks, the <block> syntax described in chapter 2. In this method, we refer to the string abc by prefixing with the character #, a positive integer indicating the length, the letter q, and the characters of the string, i.e. #3qabc
A third way of referring to strings is to use the listof function. For example, we can denote the string abc by a term of the form (listof #\a #\b #\c).
The advantage of the listof representation over the preceding representations is that it allows us to quantify over characters within strings. For example, the following sentence says that all 3 character strings beginning with a and ending with a are nice.