next up previous contents
Next: NDL scripts Up: Natural Deduction Language Previous: Using NDL in batch   Contents

Input phrases

An input phrase is one of the following:
  1. A deduction $D$. The syntax and semantics of deductions will be covered in Section 1.7 and Section 1.8, respectively. (Terminological note: in this document the terms ``deduction'' and ``proof'' will be used interchangeably.)
  2. A signature declaration $S$. These are covered in Section 1.4.
  3. An assertion. This is simply a string of the form assert $F_1, \ldots, F_n$, where each $F_i$ is a formula (formulas are discussed in Section 1.6).
  4. A file-loading directive. This is simply a string of the form

    \begin{displaymath}{\tt load } \;\: \mbox{\em filename\/}\end{displaymath}

    where filename is the name of a file in the current directory. Presumably, filename will contain a NDL script (see Section 1.3). Executing a file-loading directive has the effect of opening up the file and processing all the phrases contained in it sequentially, sending the output to the output text area as it is generated. A file can also be loaded via the GUI, by choosing Load under File at the top menu.

next up previous contents
Next: NDL scripts Up: Natural Deduction Language Previous: Using NDL in batch   Contents
2004-08-04