and adds their contents to the current theory.
Input files define a first-order theory given in the form of general clauses. Input files may also specify a reduction ordering and other meta-logical directives that serve to guide the saturation process. Before reading the details of this section, you may want to look at a few examples of input files first.
Saturate (from version 2.4 onwards) also accepts input files in Otter format or in TPTP format (with include declarations and input-clause facts). From version 2.5 onwards clauses may consist of general literals which are arbitrary, signed first-order formulas, possibly with quantifiers.
More precisely, input files consist of sequences of clauses, together with optional
Following the conventions for Prolog terms, each item must be terminated by a dot ``.'' . Terms and lists of items are to be written in Prolog notation. Comments are written as in Prolog, that is, a single line of comment is indicated by a leading ``%'' character. Other comments are included in ``/*'' and ``*/'' brackets.
We suggest that meta-logical directives be kept separate from theory presentations. How to achieve such separation is described below.