Next: NDL scripts
Up: Natural Deduction Language
Previous: Using NDL in batch
  Contents
An input phrase is one of the following:
- A deduction
. 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.)
- A signature declaration
. These are covered in
Section 1.4.
- An assertion. This is simply a string of the form
assert
, where each
is a formula
(formulas are discussed in Section 1.6).
- A file-loading directive. This is simply a string of
the form
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: NDL scripts
Up: Natural Deduction Language
Previous: Using NDL in batch
  Contents
2004-08-04