next up previous contents
Next: Formulas Up: Natural Deduction Language Previous: Signature declarations   Contents


Terms

A variable is any identifier that is neither a reserved word (such as assume or exists) nor a symbol (constant, function, or relation). We will use the letters \bgroup\color{red}$x, y, z$\egroup, and \bgroup\color{red}$w$\egroup as typical variables. A term is either a constant symbol, or a variable, or else it is an expression of the form f( \bgroup\color{red}$t_1$\egroup,..., \bgroup\color{red}$t_n$\egroup), where f is a function symbol of arity \bgroup\color{red}$n$\egroup and each \bgroup\color{red}$t_i$\egroup is a term. We will use the letters \bgroup\color{red}$s$\egroup and \bgroup\color{red}$t$\egroup as typical variables. For instance, joe, father(joe), and average(x,y) are all legal terms. NDL allows infix syntax for all binary function symbols, e.g. x average y and 2 + 5 are alternative notations for average(x,y) and +(2,5). Subexpressions in nested infix applications must be parenthesized, e.g., 2 * (5 + x).

2004-08-06