The SCAN program itself uses the Otter parser. 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. A recent description of SCAN's syntax can be found in Appendix A of Engel (1996).
Otter recognizes two basic types of statement: clauses and formulas. Clauses are simple disjunctions whose variables are implicitly universally quantified. Otter's inferences operate on clauses. Formulas are firstorder statements without free variables  all variables are explicitly quantified. When formulas are input, Otter immediately translates them to clauses.
%
.
All characters from the first %
on a line to the end of the
line are ignored. Comments can occur within terms. Comments are not
echoed to the output file.
$
, and
_
.
Names can be used for variables, constants and function symbols.
Determining whether a name is a constant or a variable depends
on the context of the term. If it occurs in a clause, the symbol
determines the type: the default rule is that a name is a
variable if it starts with u,v,w,x,y,z
.
If the flag
_
. (Therefore, variables in clauses
must be ordinary names.) A name in a formula is a variable if
and only if it is bound by a quantifier.
The pure way of writing complex terms and atoms is with standard application in
f(a,b,c)
and
=(f(x,e),x)
. If all subterms of a term are written with
standard application, the term is in pure prefix form.
Whitespace (spaces, tabs, newlines, and comments) can appear in
standard application terms anywhere except between a function or
predicate symbol and its opening parenthesis.
=
. In addition, a negated
equality, (a=b)
can be abbreviated a!=b
.

and

, respectively.
Although clauses can be written in pure prefix form, with 
as a
unary symbol and 
as a binary symbol, they are rarely written
that way. Instead, they are almost always written in infix form, without
parentheses. For example, the following is a clause in both forms.
((a),(=(b1,b2),(=(c1,c2))))
a  b1=b2  c1!=c2


&
>
<>
exists
all
all x P(x).
all x y exists z (P(x,y,z)  Q(x,z)).
all x (P(x) & Q(x) & R(x) > S(x)).
all x all y all z p(x,y,z)
all x y z p(x,y,z).
&
and 
extra parentheses can be dropped. Moreover, a default precedence on
the logic symbols allows us to drop more parentheses:
<>
has the same precedence as >
,
and the rest in decreasing order are 
, &
,

.
Greater precedence means closer to the root of the term (i.e., larger scope).
For example,
p  q & r > s  t
(p  ((q) & r)) > ((s)  t)
When in doubt about how a particular string will be parsed, one can simply add additional parentheses and/or test the string by having Otter read it and then display it in pure prefix form.
Important: All clauses and formulae have to be terminated with a period.