2 Input Syntax

The grammar in this section uses uppercase words for nonterminal symbols, allowing also hyphens. All other characters stand for themselves, with the following exceptions:

• `::=' and `|' are generally used as meta-notation, as in BNF;
• A string of characters enclosed in double quotation marks `"..."' always stands for the enclosed characters themselves;
• `N t...t N' indicates one or more repetitions of the symbol N separated by the symbol t (which is usually a terminal symbol, e.g. a comma or semicolon);
• `N...' is simply one or more repetitions of N;
• `var/vars' indicates that the singular and plural forms may be used interchangeably, and similarly for other keywords; `end/' indicates that the use of `end' is optional, and similarly for semicolons: `;/'.

The given grammar for input syntax is quite ambiguous. Section 3 provides some precedence rules for disambiguation. Note that the syntax for atomic formulae and terms caters for use of mixfix notation when applying predicates and operations; however, the recognition of the exact applicative structure of these constructs is left unspecified here, since it is inherently context-dependent. When mixfix applications are not used, the disambiguation ensures that normal applications are recognized.

All changes to the concrete syntax since the previous version (23 January 1998) are indicated by a `!' on their left; (these marks will be removed in the final version).