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 first-order 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.
_. 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(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
|, 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
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).
|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.