The WWW interface sometimes forwards formulae directly to SCAN and sometimes they are filtered through a Prolog program. In order to have a common standard for both cases we choose the Otter conventions as a standard. Therefore we list the relevant parts of the Otter manual. For the full details we refer to the original Otter manual . The following remarks, however, concerns primarily the basic SCAN interface.
Clauses are simple disjunctions whose variables are implicitly universally quantified.
Otter's inferences operate on clauses. When formulas are input, Otter immediately translates them to clauses. Comments can occur within terms. Comments are not echoed to the output file. Names can be used for variables, constants and function symbols.