Next: Terms
Up: Natural Deduction Language
Previous: NDL scripts
  Contents
Signature declarations
A signature is a collection of constant symbols
and/or fuction symbols and/or relation symbols. Constant
symbols
for any
can be introduced with the phrase
For example:
Function symbols
can be introduced with the phrase
where
is the arity of
(the number of arguments
that must be supplied in an application of
).
Example:
Here average is declared to be a binary function symbol,
and father a unary one.
Relation symbols
can be introduced with the phrase
where again
is the arity of
. For instance, the phrase
declares father and male to be unary relations, likes
to be a binary relation, and between to be a ternary one.
Symbols can also be introduced via the GUI, by choosing
Signature under Options at the top menu bar.
NDL comes with certain predefined symbols:
- Predefined constant symbols: All numerals
- Predefined unary function symbols:
- Predefined binary function symbols: +, -, *, /, %,@
- Predefined binary relation symbols:
Note that NDL will ignore any attempts to redeclare
a symbol that has already been introduced.
The user can inspect the current signature at any given time
by choosing Options followed by View current signature
on the top menu bar.
Next: Terms
Up: Natural Deduction Language
Previous: NDL scripts
  Contents
2004-08-04