Function NAME

The term {tt (name $tau$)} denotes the standard name for the object denoted by the term $tau$. The standard name for an expression $tau$ is {tt (quote $tau$)}; 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 models with uncountable cardinality; consequently, it is not always possible for every object in the universe of discourse to have a unique name.)
Arity: 2