next up previous contents
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 $c_1,\ldots,c_n$ for any $n > 0$ can be introduced with the phrase

\begin{displaymath}\mbox{\tt Constants } c_1,\ldots,c_n\end{displaymath}

For example:

\begin{displaymath}\mbox{\tt Constants pi, joe, ann, d23}\end{displaymath}

Function symbols $f_1,\ldots,f_n$ can be introduced with the phrase

\begin{displaymath}\mbox{\tt Functions } f_1\mbox{\tt :}r_1,\ldots,f_n\mbox{\tt :}r_n\end{displaymath}

where $r_i$ is the arity of $f_i$ (the number of arguments that must be supplied in an application of $f_i$). Example:

\begin{displaymath}\mbox{\tt Functions father:1,average:2}\end{displaymath}

Here average is declared to be a binary function symbol, and father a unary one. Relation symbols $R_1,\ldots,R_n$ can be introduced with the phrase

\begin{displaymath}\mbox{\tt Relations } R_1\mbox{\tt :}r_1,\ldots,R_n\mbox{\tt :}r_n\end{displaymath}

where again $r_i$ is the arity of $R_i$. For instance, the phrase

\begin{displaymath}\mbox{\tt Relations father:1, male:1, likes:2, between:3}\end{displaymath}

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:
  1. Predefined constant symbols: All numerals $0, 1, 2, \ldots$
  2. Predefined unary function symbols:
  3. Predefined binary function symbols: +, -, *, /, %,@
  4. 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 up previous contents
Next: Terms Up: Natural Deduction Language Previous: NDL scripts   Contents
2004-08-04