SCAN

Syntax for formulae

The syntax for first-order formulae used in SCAN is the same as the syntax used in the Otter theorem prover.

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.

Comments
Names for Variables, Constants, Functions, and Predicates
Terms and Atoms
Literals and Clauses
Formulas

Comments

Comments can be placed in the input file by using the symbol %. 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 for Variables, Constants, Functions, and Predicates

A name is a string of alphanumerics, $, 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

prolog style variables

is set, a simple term is a variable if and only if it starts with an upper-case letter or with _. (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.

Terms and Atoms

Constants and variables are terms. An n-ary function symbol applied to n terms is also a term. An n-ary predicate symbol applied to n terms is an atom. A nullary predicate symbol (also referred to as a propositional variable) is also an atom.

The pure way of writing complex terms and atoms is with standard application in

prefix form:: the function or predicate symbol, opening parenthesis, arguments separated by commas, then closing parenthesis, for example, 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.
Infix Equality:: Some binary functions and predicates can be written in infix form; the most important is =. In addition, a negated equality, -(a=b) can be abbreviated a!=b.

Literals and Clauses

A literal is either an atom or the negation of an atom. A clause is a disjunction of literals. The built-in symbols for negation and disjunction are - 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.

Pure prefix:: |(-(a),|(=(b1,b2),-(=(c1,c2))))
Infix (abbreviated):: -a | b1=b2 | c1!=c2

Otter accepts both forms.

Formulas

The table below lists the built-in logic symbols for constructing formulas.

negation: -

disjunction: |

conjunction: &

implication: ->

equivalence: <->

existential quantification: exists

universal quantification: all

Formulas are usually written in a natural way. Here are some examples.

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)).

Note that if a formula has a string of identical quantifiers, all but the first can be dropped. For example,

all x all y all z p(x,y,z)

can be shortened to

all x y z p(x,y,z).

In expressions involving the associative operations & 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

represents

(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.