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
, and
as typical variables.
A term is either a constant symbol, or a variable, or
else it is an expression of the form f(
,...,
),
where f is a function symbol of arity
and each
is a term. We will use the letters
and
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