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


Terms

An identifier will be understood as any finite sequence of letters, digits, underscores () or dashes (-) that begins with a letter. Any identifier that is not a symbol (constant, function, or relation) will count as a variable. We will use the letters $x, y, z$, and $w$ as typical variables. A term is either a constant symbol, or a variable, or else it is an expression of the form f($t_1$,...,$t_n$), where f is a function symbol of arity $n$ and each $t_i$ is a term. We will use the letters $s$ and $t$ 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-04