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. Lexically, symbols are just identifiers, where an identifier will be understood as any finite sequence of letters, digits, or underscores () that begins with a letter.+1.3 Constant symbols \bgroup\color{red}$c_1,\ldots,c_n$\egroup for any \bgroup\color{red}$n > 0$\egroup can be introduced with the phrase

\begin{displaymath}\bgroup\color{red}\mbox{\tt Constants } c_1,\ldots,c_n\egroup\end{displaymath}

For example:

\begin{displaymath}\bgroup\color{red}\mbox{\tt Constants pi, joe, ann, d23}\egroup\end{displaymath}

Function symbols \bgroup\color{red}$f_1,\ldots,f_n$\egroup can be introduced with the phrase

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

where \bgroup\color{red}$r_i$\egroup is the arity of \bgroup\color{red}$f_i$\egroup (the number of arguments that must be supplied in an application of \bgroup\color{red}$f_i$\egroup). Example:

\begin{displaymath}\bgroup\color{red}\mbox{\tt Functions father:1,average:2}\egroup\end{displaymath}

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

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

where again \bgroup\color{red}$r_i$\egroup is the arity of \bgroup\color{red}$R_i$\egroup. For instance, the phrase

\begin{displaymath}\bgroup\color{red}\mbox{\tt Relations male:1, likes:2, between:3}\egroup\end{displaymath}

declares male to be a unary relation, 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 from the top menu bar.
next up previous contents
Next: Terms Up: Natural Deduction Language Previous: NDL scripts   Contents
2004-08-06